projects
/
cdsspec-compiler.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
0a040a5
)
minor fix
author
Peizhao Ou
<peizhaoo@uci.edu>
Tue, 14 Jan 2014 05:47:39 +0000
(21:47 -0800)
committer
Peizhao Ou
<peizhaoo@uci.edu>
Tue, 14 Jan 2014 05:47:39 +0000
(21:47 -0800)
benchmark/linuxrwlocks/linuxrwlocks.c
patch
|
blob
|
history
diff --git
a/benchmark/linuxrwlocks/linuxrwlocks.c
b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0f52b66b65f5887ed5e0ee6955d079eb3ac97b51..f3d0896c817b1eefb514bd312cd27b462e240c9b 100644
(file)
--- a/
benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/
benchmark/linuxrwlocks/linuxrwlocks.c
@@
-52,9
+52,6
@@
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 -> Write_Lock
- Read_Unlock -> Write_Trylock(HB_Write_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)
@@
-149,7
+146,7
@@
static inline void write_lock(rwlock_t *rw)
@Begin
@Interface: Read_Trylock
@Commit_point_set:
@Begin
@Interface: Read_Trylock
@Commit_point_set:
- Read_Trylock_Point
+ Read_Trylock_
Succ_Point | Read_Trylock_Fail_
Point
@Condition:
writer_lock_acquired == false
@HB_condition:
@Condition:
writer_lock_acquired == false
@HB_condition:
@@
-166,13
+163,27
@@
static inline int read_trylock(rwlock_t *rw)
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
/**
@Begin
- @
Commit_point_define_check
: true
- @Label:Read_Trylock_Point
+ @
Potential_commit_point
: true
+ @Label:
Potential_
Read_Trylock_Point
@End
*/
@End
*/
- if (priorvalue > 0)
+ if (priorvalue > 0) {
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Label: Read_Trylock_Succ_Point
+ @Potential_commit_point_label: Potential_Read_Trylock_Point
+ @End
+ */
return 1;
return 1;
-
+ }
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Label: Read_Trylock_Fail_Point
+ @Potential_commit_point_label: Potential_Read_Trylock_Point
+ @End
+ */
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
return 0;
}
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
return 0;
}
@@
-181,7
+192,7
@@
static inline int read_trylock(rwlock_t *rw)
@Begin
@Interface: Write_Trylock
@Commit_point_set:
@Begin
@Interface: Write_Trylock
@Commit_point_set:
- Write_Trylock_Point
+ Write_Trylock_
Succ_Point | Write_Trylock_Fail_
Point
@Condition:
!writer_lock_acquired && reader_lock_cnt == 0
@HB_condition:
@Condition:
!writer_lock_acquired && reader_lock_cnt == 0
@HB_condition:
@@
-198,13
+209,27
@@
static inline int write_trylock(rwlock_t *rw)
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
/**
@Begin
- @
Commit_point_define_check
: true
- @Label: Write_Trylock_Point
+ @
Potential_commit_point
: true
+ @Label:
Potential_
Write_Trylock_Point
@End
*/
@End
*/
- if (priorvalue == RW_LOCK_BIAS)
+ if (priorvalue == RW_LOCK_BIAS) {
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Label: Write_Trylock_Succ_Point
+ @Potential_commit_point_label: Potential_Write_Trylock_Point
+ @End
+ */
return 1;
return 1;
-
+ }
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Label: Write_Trylock_Fail_Point
+ @Potential_commit_point_label: Potential_Write_Trylock_Point
+ @End
+ */
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
return 0;
}
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
return 0;
}