+++ /dev/null
-#ifndef _SEQLOCK_H
-#define _SEQLOCK_H
-
-#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;
-
-typedef void* (*read_func_ptr_t)(void*);
-
-/**
- Properties to check:
- Every read will read the up-to-date value, and only one thread can be
- writing.
-*/
-
-/**
- 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
- Boehm's paper <<Can seqlocks get along with programming language memory
- models>>.
-
- Interesting thing in the read() function is the memory ordering we should
- impose there. In Hans Boehm's paper, he presents 3 ways to do it. We will
- try to use the fences one here as a special case to check programs written
- with C++ fences.
-*/
-
-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:
- // 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_int _data1;
- atomic_int _data2;
-
- /**
- @Begin
- @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
- */
-
- public:
- seqlock() {
- _data1.store(0, memory_order_relaxed);
- _data2.store(0, memory_order_relaxed);
- _seq.store(0, memory_order_relaxed);
-
- /**
- @Begin
- @Entry_point
- @End
- */
- }
-
- ~seqlock() {}
-
- /**
- @Begin
- @Interface: Read
- @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:
- _read(*d1, *d2);
- @End
- */
- void read(int *d1, int *d2) {
- while (true) {
- /**** 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);
-
- 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();
- }
- }
- }
-
- /**
- @Begin
- @Interface: Write
- @Commit_point_set: WritePoint
- @ID: getID(d1, d2);
- @Action:
- //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(int d1, int d2) {
- int seq;
- while (true) {
- /**** admissibility ****/
- seq = _seq.load(memory_order_acquire);
- if (seq & 0x1) {
- thrd_yield();
- continue;
- }
- bool succ = _seq.compare_exchange_strong(seq, seq + 1,
- memory_order_relaxed, memory_order_relaxed);
- if (succ) {
- break;
- } else {
- thrd_yield();
- }
- }
- /**** 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_check: true
- @Label: WritePoint
- @End
- */
- }
-};
-/**
- @Begin
- @Class_end
- @End
-*/
-
-
-#endif
projects / cdsspec-compiler.git / blobdiff