#ifndef _SEQLOCK_H
#define _SEQLOCK_H
-#include <atomic>
+#include <stdatomic.h>
+#include <unrelacy.h>
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
using namespace std;
writing.
*/
-
-/**
- @Begin
- @Global_define:
- Type *__data_ptr = NULL;
- bool __is_writing = false;
-
- static bool _is_equals(void* ptr1, void* ptr2) {
- //... Should be defined to check if the internal data equals
- }
-
- @Happens-before:
- Init -> Read
- Init -> Write
- Write -> Write
- Write -> Read
- @End
-*/
-
/**
Fixed the write to be lock-free. Use a CAS in the write instead of using the
mutex. There are a couple options for the implementation according to Hans
with C++ fences.
*/
-template<typename Type>
+typedef struct Data {
+ int data1, data2;
+} Data;
+
+bool equal(int64_t p1, int64_t p2) {
+ if (!p1 || !p2)
+ return false;
+ Data *d1 = (Data*) p1;
+ Data *d2 = (Data*) p2;
+ if (d1->data1 == d2->data1 &&
+ d1->data2 == d2->data2) {
+ return true;
+ } else {
+ return false;
+ }
+}
+
+
+/**
+ @Begin
+ @Class_begin
+ @End
+*/
class seqlock {
private:
- // To make the write lock-free, we don't need the mutex here.
- // Mutex to write exclusively
-
// Sequence for reader consistency check
atomic_int _seq;
+
// The shared data structure to be protected;
// It needs to be atomic to avoid data races
- atomic<Type*> _data;
-
- // This function is to check if the objects pointed by the two pointer are
- // the same; it is only used for checking the correctness
- bool is_equal(void *ptr1, void *ptr2) {
- // return ptr1 == NULL ? false : ptr1->equals(ptr2);
- }
+ atomic_int _data1;
+ atomic_int _data2;
- public:
/**
@Begin
- @Interface: Init
- @Commit_point_set: Init_Point
- @Action:
- @Code:
- __data_ptr = data;
+ @Options:
+ LANG = CPP;
+ CLASS = seqlock;
+ @Global_define:
+ @DeclareVar:
+ IntegerList *set;
+ @InitVar:
+ set = createIntegerList();
+ Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+ d->data1 = 0;
+ d->data2 = 0;
+ push_back(set, (int64_t) d);
+ @Finalize:
+ if (set)
+ destroyIntegerList(set);
+ return true;
+ @DefineFunc:
+ // This is a trick to get unique id
+ // The testcase should have a unique sum
+ call_id_t getID(int64_t d1, int64_t d2) {
+ return d1 + d2;
+ }
+ @DefineFunc:
+ bool print(int64_t p) {
+ Data *d = (Data*) p;
+ model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
+ }
+ @DefineFunc:
+ void _write(int64_t d1, int64_t d2) {
+ Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+ d->data1 = d1;
+ d->data2 = d2;
+ push_back(set, (int64_t) d);
+ }
+ @DefineFunc:
+ bool _read(int d1, int d2) {
+ Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+ d->data1 = d1;
+ d->data2 = d2;
+ bool hasElem = has_elem_by_value(set, (int64_t) d, &equal);
+ return hasElem;
+ }
+ @Happens_before:
+ Write -> Write
+ Write -> Read
+ @Commutativity: Write <-> Read: true
@End
*/
- seqlock(Type *data) {
- _data.store(data, memory_order_relaxed);
- _seq.store(0, memory_order_release);
+
+ public:
+ seqlock() {
+ _data1.store(0, memory_order_relaxed);
+ _data2.store(0, memory_order_relaxed);
+ _seq.store(0, memory_order_relaxed);
+
/**
- # Initialization code
- @Begin
- @Commit_point_check_define: true
- @Label: Init_Point
+ @Begin
+ @Entry_point
@End
*/
}
/**
@Begin
@Interface: Read
- @Commit_point_set: Read_Success_Point
- @Action:
- @Code:
- void *_Old_data_ptr = __data_ptr;
+ @Commit_point_set: ReadPoint
+ @ID: getID(*d1, *d2)
+ //@Action:
+ //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(*d1, *d2),
+ // *d1, *d2);
+ //do_by_value(set, &print);
@Post_check:
- _is_equal(read_func(_Old_data_ptr), __RET__)
+ _read(*d1, *d2);
@End
*/
- void* read(read_func_ptr_t read_func) {
+ void read(int *d1, int *d2) {
while (true) {
- int old_seq = _seq.load(memory_order_acquire);
- if (old_seq % 2 == 1) continue;
- // A customized read of something return a pointer to it
- // Potential data race, should be atomic
- void *res = read_func(_data.load(memory_order_relaxed));
- // This is subtle to use an acquire fence here
- // What we actually need is a #LoadLoad fence
+ /**** SPEC (sequential) ****/
+ int seq1 = _seq.load(memory_order_acquire);
+ printf("seq1=%d\n", seq1);
+ if (seq1 & 0x1 == 1) {
+ thrd_yield();
+ continue;
+ }
+ // Try to read the data
+ *d1 = _data1.load(memory_order_relaxed);
+ *d2 = _data2.load(memory_order_relaxed);
+ /**** SPEC (sequential) ****/
atomic_thread_fence(memory_order_acquire);
- int new_seq;
- if ((new_seq = _seq.load(memory_order_relaxed)) == old_seq) {
- /**
- @Begin
- @Commit_point_check_define: __ATOMIC_RET__ == old_seq
- @Label: Read_Success_Point
- @End
- */
- return res;
+
+ printf("d1=%d\n", *d1);
+ printf("d2=%d\n", *d2);
+ // Now doulbe check nothing got updated
+ int seq2 = _seq.load(memory_order_relaxed);
+ /**
+ @Begin
+ @Commit_point_define_check: seq1 == seq2
+ @Label: ReadPoint
+ @End
+ */
+ printf("seq2=%d\n", seq1);
+ if (seq1 == seq2) { // Good to go
+ printf("Result: d1=%d, d2=%d\n", *d1, *d2);
+ return;
+ } else {
+ thrd_yield();
}
- // _data has been updated, read should retry
}
}
/**
@Begin
@Interface: Write
- @Commit_point_set: Write_Success_Point
+ @Commit_point_set: WritePoint
+ @ID: getID(d1, d2);
@Action:
- @Code:
- __data_ptr = new_data;
+ //model_print("Write_ID = %d, d1=%d, d2=%d\n", getID(d1, d2), d1, d2);
+ _write(d1, d2);
+ //do_by_value(set, &print);
@End
*/
-
- void write(Type *new_data) {
+ void write(int d1, int d2) {
+ int seq;
while (true) {
- // This might be a relaxed too
- // Should think about how to read the lo
- int old_seq = _seq.load(memory_order_acquire);
- if (old_seq % 2 == 1) {
- // Backoff, another thread is writing
- //thrd_yield();
- continue; // Retry
+ /**** admissibility ****/
+ seq = _seq.load(memory_order_acquire);
+ if (seq & 0x1) {
+ thrd_yield();
+ continue;
}
- // Should be relaxed!!!
- if (_seq.compare_exchange_strong(old_seq, old_seq + 1,
- memory_order_relaxed, memory_order_relaxed))
+ bool succ = _seq.compare_exchange_strong(seq, seq + 1,
+ memory_order_relaxed, memory_order_relaxed);
+ if (succ) {
break;
+ } else {
+ thrd_yield();
+ }
}
- // Should be a store release, to synchronize with the fence!!!
- _data.store(new_data, memory_order_release);
+ /**** SPEC (sequential) ****/
+ atomic_thread_fence(memory_order_release);
+ _data1.store(d1, memory_order_relaxed);
+ _data2.store(d2, memory_order_relaxed);
+ // Should be a store release!!!
+ /**** admissibility ****/
_seq.fetch_add(1, memory_order_release);
/**
@Begin
- @Commit_point_define: true
- @Label: Write_Success_Point
+ @Commit_point_define_check: true
+ @Label: WritePoint
@End
*/
}
};
+/**
+ @Begin
+ @Class_end
+ @End
+*/
#endif
projects / cdsspec-compiler.git / blobdiff