seqlock/seqlock.cc

   1 #include <stdatomic.h>
   2 #include <threads.h>
   3 #include "seqlock.h"
   4
   5 seqlock::seqlock() {
   6         atomic_init(&_seq, 0);
   7         atomic_init(&_data1, 0);
   8         atomic_init(&_data2, 0);
   9 }
  10
  11 /** @DeclareState: int data1;
  12                 int data2; */
  13
  14 void seqlock::read(int *data1, int *data2) {
  15         while (true) {
  16         // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
  17         // "memory_order_relaxed", run "make" to recompile, and then run:
  18         // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
  19
  20                 /**********    Detected Correctness (testcase1)    **********/
  21                 int old_seq = _seq.load(memory_order_acquire); // acquire
  22                 if (old_seq % 2 == 1) {
  23             thrd_yield();
  24             continue;
  25         }
  26
  27                 // Acquire ensures that the second _seq reads an update-to-date value
  28                 *data1 = _data1.load(memory_order_relaxed);
  29                 *data2 = _data2.load(memory_order_relaxed);
  30                 /** @OPClearDefine: true */
  31
  32         // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
  33         // "memory_order_relaxed", run "make" to recompile, and then run:
  34         // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
  35                 /**********    Detected Correctness (testcase1)    **********/
  36                 atomic_thread_fence(memory_order_acquire);
  37                 if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
  38             thrd_yield();
  39                         return;
  40                 }
  41         }
  42 }
  43
  44
  45 void seqlock::write(int data1, int data2) {
  46         while (true) {
  47                 // #1: either here or #2 must be acquire
  48         // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to
  49         // "memory_order_relaxed", run "make" to recompile, and then run:
  50         // "./run.sh ./seqlock/testcase2 -m2 -y -u3 -x1000 -tSPEC"
  51                 /**********    Detected Correctness (testcase2 with -y -x1000)    **********/
  52                 int old_seq = _seq.load(memory_order_acquire); // acquire
  53                 if (old_seq % 2 == 1) {
  54             thrd_yield();
  55                         continue; // Retry
  56         }
  57
  58                 // #2
  59                 if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
  60                         memory_order_relaxed, memory_order_relaxed)) {
  61             thrd_yield();
  62                         break;
  63                 }
  64         }
  65
  66         // Update the data. It needs to be release since this version use
  67         // relaxed CAS in write(). When the first load of _seq reads the realaxed
  68         // CAS update, it does not form synchronization, thus requiring the data to
  69         // be acq/rel. The data in practice can be pointers to objects.
  70
  71     // XXX-injection-#4: Weaken the parameter "memory_order_release" to
  72     // "memory_order_relaxed", run "make" to recompile, and then run:
  73     // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
  74         /**********    Detected Correctness (testcase1)    **********/
  75         atomic_thread_fence(memory_order_release);
  76         _data1.store(data1, memory_order_relaxed);
  77         _data2.store(data2, memory_order_relaxed);
  78         /** @OPDefine: true */
  79
  80     // XXX-injection-#5: Weaken the parameter "memory_order_release" to
  81     // "memory_order_relaxed", run "make" to recompile, and then run:
  82     // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC"
  83         /**********    Detected Correctness (testcase1)    **********/
  84         _seq.fetch_add(1, memory_order_release); // release
  85 }
  86
  87 /** C Interface */
  88
  89 /** @Transition: STATE(data1) = data1;
  90                 STATE(data2) = data2; */
  91 void write(seqlock *lock, int data1, int data2) {
  92         lock->write(data1, data2);
  93 }
  94
  95
  96 /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */
  97 void read(seqlock *lock, int *data1, int *data2) {
  98         lock->read(data1, data2);
  99 }