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: This cannot be detected unless when we only have a single data
  17                 // varaible since that becomes a plain load/store. However, when we have
  18                 // multiple data pieces, we will detect the inconsitency of the data.
  19                 /**********    Detected Correctness (testcase1)    **********/
  20                 int old_seq = _seq.load(memory_order_acquire); // acquire
  21                 if (old_seq % 2 == 1) {
  22             thrd_yield();
  23             continue;
  24         }
  25
  26                 // Acquire ensures that the second _seq reads an update-to-date value
  27                 /**********    Detected Correctness (testcase1)    **********/
  28                 *data1 = _data1.load(memory_order_relaxed);
  29                 *data2 = _data2.load(memory_order_relaxed);
  30                 /** @OPClearDefine: true */
  31                 /**********    Detected Correctness (testcase1)    **********/
  32                 atomic_thread_fence(memory_order_acquire);
  33                 if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed
  34             thrd_yield();
  35                         return;
  36                 }
  37         }
  38 }
  39
  40
  41 void seqlock::write(int data1, int data2) {
  42         while (true) {
  43                 // #1: either here or #2 must be acquire
  44                 /**********    Detected Correctness (testcase2 with -y -x1000)    **********/
  45                 int old_seq = _seq.load(memory_order_acquire); // acquire
  46                 if (old_seq % 2 == 1) {
  47             thrd_yield();
  48                         continue; // Retry
  49         }
  50
  51                 // #2
  52                 if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
  53                         memory_order_relaxed, memory_order_relaxed)) {
  54             thrd_yield();
  55                         break;
  56                 }
  57         }
  58
  59         // XXX: Update the data. It needs to be release since this version use
  60         // relaxed CAS in write(). When the first load of _seq reads the realaxed
  61         // CAS update, it does not form synchronization, thus requiring the data to
  62         // be acq/rel. The data in practice can be pointers to objects.
  63         /**********    Detected Correctness (testcase1)    **********/
  64         atomic_thread_fence(memory_order_release);
  65         _data1.store(data1, memory_order_relaxed);
  66         _data2.store(data2, memory_order_relaxed);
  67         /** @OPDefine: true */
  68
  69         /**********    Detected Admissibility (testcase1)    **********/
  70         _seq.fetch_add(1, memory_order_release); // release
  71 }
  72
  73 /** C Interface */
  74
  75 /** @Transition: STATE(data1) = data1;
  76                 STATE(data2) = data2; */
  77 void write(seqlock *lock, int data1, int data2) {
  78         lock->write(data1, data2);
  79 }
  80
  81
  82 /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */
  83 void read(seqlock *lock, int *data1, int *data2) {
  84         lock->read(data1, data2);
  85 }