projects
/
cdsspec-compiler.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
need to fix deque
[cdsspec-compiler.git]
/
benchmark
/
linuxrwlocks
/
linuxrwlocks.c
diff --git
a/benchmark/linuxrwlocks/linuxrwlocks.c
b/benchmark/linuxrwlocks/linuxrwlocks.c
index 6341c4c1fcf336474ea9008b5e84b3e083b0968f..0a1a7b203f02f6477623c5ed8f64765ca341a10a 100644
(file)
--- a/
benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/
benchmark/linuxrwlocks/linuxrwlocks.c
@@
-61,6
+61,11
@@
typedef union {
@Happens_before:
# Since commit_point_set has no ID attached, A -> B means that for any B,
# the previous A happens before B.
@Happens_before:
# Since commit_point_set has no ID attached, A -> B means that for any B,
# the previous A happens before B.
+ Read_Unlock -> Read_Lock
+ Read_Unlock -> Write_Lock
+ Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+ Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
Write_Unlock -> Write_Lock
Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
Write_Unlock -> Write_Lock
Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
@@
-202,20
+207,17
@@
static inline int read_trylock(rwlock_t *rw)
@Interface: Write_Trylock
@Commit_point_set:
Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
@Interface: Write_Trylock
@Commit_point_set:
Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
- @Condition:
- !writer_lock_acquired && reader_lock_cnt == 0
@HB_condition:
HB_Write_Trylock_Succ :: __RET__ == 1
@Action:
@HB_condition:
HB_Write_Trylock_Succ :: __RET__ == 1
@Action:
- if (__
COND_SAT__
)
+ if (__
RET__ == 1
)
writer_lock_acquired = true;
writer_lock_acquired = true;
- @Post_check:
- __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
@End
*/
static inline int write_trylock(rwlock_t *rw)
{
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
@End
*/
static inline int write_trylock(rwlock_t *rw)
{
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+ //model_print("write_trylock: priorvalue: %d\n", priorvalue);
/**
@Begin
@Potential_commit_point_define: true
/**
@Begin
@Potential_commit_point_define: true