-/**
- @Begin
- @Options:
- LANG = C;
- @Global_define:
- @DeclareVar:
- bool writer_lock_acquired;
- int reader_lock_cnt;
- @InitVar:
- writer_lock_acquired = false;
- reader_lock_cnt = 0;
- @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 -> Read_Lock
- Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
-