edits

[cdsspec-compiler.git] / benchmark / linuxrwlocks / linuxrwlocks.c

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 1f7059f828004926926c0b0682b52cf909804c9d..03a292b3b6978860bb355081dc7d274a6ca1f3eb 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -47,31 +47,11 @@ typedef union {
        auxiliary check since it is an extra rule for how the interfaces should called.
 */
 
-/**
-       @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)
-       
+/** @DeclareState:
+               bool writer_lock_acquired;
+               int reader_lock_cnt;
+       @Initial: writer_lock_acquired = false;
+               reader_lock_cnt = 0;
        @Commutativity: Read_Lock <-> Read_Lock: true
        @Commutativity: Read_Lock <-> Read_Unlock: true
        @Commutativity: Read_Lock <-> Read_Trylock: true
@@ -89,7 +69,6 @@ typedef union {
        @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
        @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
        @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
-       @End
 */
 
 static inline int read_can_lock(rwlock_t *lock)