/**
@Begin
@Interface: Read_Lock
- @Commit_point_set:
- Read_Lock_Success_1 | Read_Lock_Success_2
- @Check:
- !writer_lock_acquired
- @Action:
- reader_lock_cnt++;
+ @Commit_point_set: Read_Lock_Success_1 | Read_Lock_Success_2
+ @Check: !writer_lock_acquired
+ @Action: reader_lock_cnt++;
@End
*/
static inline void read_lock(rwlock_t *rw)
/**
@Begin
@Interface: Write_Lock
- @Commit_point_set:
- Write_Lock_Success_1 | Write_Lock_Success_2
- @Check:
- !writer_lock_acquired && reader_lock_cnt == 0
- @Action:
- writer_lock_acquired = true;
+ @Commit_point_set: Write_Lock_Success_1 | Write_Lock_Success_2
+ @Check: !writer_lock_acquired && reader_lock_cnt == 0
+ @Action: writer_lock_acquired = true;
@End
*/
static inline void write_lock(rwlock_t *rw)
/**
@Begin
@Interface: Read_Trylock
- @Commit_point_set:
- Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
- @Condition:
- writer_lock_acquired == false
- @HB_condition:
- HB_Read_Trylock_Succ :: __RET__ == 1
+ @Commit_point_set: Read_Trylock_Succ_Point | Read_Trylock_Fail_Point
+ //@Condition: writer_lock_acquired == false
+ @HB_condition: HB_Read_Trylock_Succ :: __RET__ == 1
@Action:
if (__COND_SAT__)
reader_lock_cnt++;
- @Post_check:
- __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
+ @Post_check: __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
@End
*/
static inline int read_trylock(rwlock_t *rw)
/**
@Begin
@Interface: Write_Trylock
- @Commit_point_set:
- Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
- @HB_condition:
- HB_Write_Trylock_Succ :: __RET__ == 1
+ @Commit_point_set: Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
+ @HB_condition: HB_Write_Trylock_Succ :: __RET__ == 1
@Action:
if (__RET__ == 1)
writer_lock_acquired = true;
@Begin
@Interface: Read_Unlock
@Commit_point_set: Read_Unlock_Point
- @Check:
- reader_lock_cnt > 0 && !writer_lock_acquired
- @Action:
- reader_lock_cnt--;
+ @Check: reader_lock_cnt > 0 && !writer_lock_acquired
+ @Action: reader_lock_cnt--;
@End
*/
static inline void read_unlock(rwlock_t *rw)
@Begin
@Interface: Write_Unlock
@Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
- @Check:
- reader_lock_cnt == 0 && writer_lock_acquired
- @Action:
- writer_lock_acquired = false;
+ @Check: reader_lock_cnt == 0 && writer_lock_acquired
+ @Action: writer_lock_acquired = false;
@End
*/
static inline void write_unlock(rwlock_t *rw)