@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)
@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:
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_define: true
+ @Label: Potential_Read_Trylock_Point
@End
*/
- if (priorvalue > 0)
+ if (priorvalue > 0) {
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Potential_Read_Trylock_Point
+ @Label: Read_Trylock_Succ_Point
+ @End
+ */
return 1;
-
+ }
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Potential_Read_Trylock_Point
+ @Label: Read_Trylock_Fail_Point
+ @End
+ */
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
return 0;
}
@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:
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_define: true
+ @Label: Potential_Write_Trylock_Point
@End
*/
- if (priorvalue == RW_LOCK_BIAS)
+ if (priorvalue == RW_LOCK_BIAS) {
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Potential_Write_Trylock_Point
+ @Label: Write_Trylock_Succ_Point
+ @End
+ */
return 1;
-
+ }
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Potential_Write_Trylock_Point
+ @Label: Write_Trylock_Fail_Point
+ @End
+ */
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
return 0;
}