LANG = CPP;
CLASS = mcs_mutex;
@Global_define:
- @DeclareVar:
- bool _lock_acquired;
- @InitVar:
- _lock_acquired = false;
- @Happens_before:
- Unlock -> Lock
+ @DeclareVar: bool _lock_acquired;
+ @InitVar: _lock_acquired = false;
+ @Happens_before: Unlock -> Lock
@End
*/
@Begin
@Interface: Lock
@Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
- @Check:
- _lock_acquired == false;
- @Action:
- _lock_acquired = true;
+ @Check: _lock_acquired == false;
+ @Action: _lock_acquired = true;
@End
*/
void lock(guard * I) {
/**
@Begin
@Interface: Unlock
- @Commit_point_set:
- Unlock_Point_Success_1 | Unlock_Point_Success_2
- @Check:
- _lock_acquired == true
- @Action:
- _lock_acquired = false;
+ @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
+ @Check: _lock_acquired == true
+ @Action: _lock_acquired = false;
@End
*/
void unlock(guard * I) {