int ll_val;        // value read by LL
int val;           // current value of memory cell
int mark;          // mark to trigger slow path in stores
int listed;        // abstract representation of "locked list"
int sc_failure;    // did SC succeed or fail?

/* common implementation of store-conditional */
#define SC                                           \
   atomic {                                          \
       sc_failure = !listed;                         \
       assert(sc_failure || val == ll_val);          \
       if :: sc_failure -> skip;                     \
          :: else -> mark = 0; listed = 0; val = 2;  \
       fi;                                           \
   }

// trivial implementation, obviously broken - does not even try
#if 0
#define LL                                    \
   listed = 1;                                \
   ll_val = val;                              \
   mark = 1;

#define STORE                                 \
   val = 1
#endif

// -------------------------------------------------------------------

// broken implementation #1
// STORE can read the mark before LL has set it.  If it stores
// the new value after LL has read the memory, SC will not
// notice the conflict.

#if 0
#define LL                                    \
   ll_val = val;                              \
   atomic {                                   \
     listed = 1;                              \
     mark = 1;                                \
   }

#define STORE                                     \
   if :: mark -> atomic { listed = 0; mark = 0; } \
      :: else -> skip;                            \
   fi;                                            \
   val = 1
#endif

// -------------------------------------------------------------------

// broken implementation #2
// If STORE reads the mark before LL has set it, SC will not
// notice the conflict.

#if 0
#define LL                                    \
   atomic {                                   \
     listed = 1;                              \
     ll_val = val;                            \
     mark = 1;                                \
   }

#define STORE                                 \
   if :: mark -> atomic { listed = 0; mark = 0; } \
      :: else -> skip;                            \
   fi;                                            \
   val = 1
#endif

// -------------------------------------------------------------------

// This works but uses transactional memory in STORE

#if 1
#define LL                                    \
   listed = 1;                                \
   mark = 1;                                  \
   ll_val = val;                              \

#define STORE                                              \
  atomic {                                                 \
    if :: mark -> slow = 1;                                \
       :: else -> val = 1;                                 \
    fi                                                     \
  }                                                        \
  if :: slow -> atomic { mark = 0; val = 1; listed = 0; }; \
     :: else -> skip;                                      \
  fi

#endif

active proctype llsc()
{
   LL;
   SC;
}

active proctype store()
{
   int slow;
   STORE;
}