#include <atomic>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
-using namespace std;
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
+#include "librace.h"
/**
This is an example about how to specify the correctness of the
read-copy-update synchronization mechanism.
*/
-// Properties to check:
-
-
-typedef void* (*read_func_ptr_t)(void*);
+typedef struct Data {
+ int data1;
+ int data2;
+} Data;
-template <typename Type>
-class rcu {
- /**
- @Begin
- @Global_define:
- Type *__cur_data;
-
- static bool equals(void *ptr1, void *ptr2) {
- // ...
- // Return if the two data instances pointed to equals to each
- // other
+atomic<Data*> data;
+
+/**
+ @Begin
+ @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);
+ }
+ 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;
}
+ }
+ @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(Data *res) {
+ bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
+ return hasElem;
+ }
+ @Happens_before:
+ Write -> Read
+ Write -> Write
+ @Commutativity: Write <-> Read: true
+ @End
+*/
- @Happens-before:
- Write -> Read
- Write -> Write
- @End
- */
-private:
- atomic<Type*> _data;
-
- public:
+/**
+ @Begin
+ @Interface: Read
+ @Commit_point_set: Read_Success_Point
+ @ID: getID(__RET__->data1, __RET__->data2)
+ //@Action:
+ //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
+ // __RET__->data2), __RET__->data1, __RET__->data2);
+ //do_by_value(set, &print);
+ @Post_check:
+ _read(__RET__);
+ @End
+*/
+Data* read() {
+ /********** SPEC (sync) **********/
+ Data *res = data.load(memory_order_acquire);
+ //load_32(&res->data1);
/**
@Begin
- @Interface: Read
- @Commit_point_set: Read_Success_Point
- @Action:
- @Code:
- void *_Old_Data = __cur_data;
- @Post_check:
- equals(__RET__, _Old_Data->read())
+ @Commit_point_define_check: true
+ @Label: Read_Success_Point
@End
*/
- void* read() {
- void *res = NULL;
- Type *cur_data_ptr = _data.load(memory_order_acquire);
+ return res;
+}
+
+/**
+ @Begin
+ @Interface: Write
+ @Commit_point_set: Write_Success_Point
+ @ID: getID(d1, d2);
+ @Action:
+ //model_print("Write_ID = %d\n", getID(d1, d2));
+ _write(d1, d2);
+ @End
+*/
+Data* write(int d1, int d2) {
+ bool succ = false;
+ Data *tmp = (Data*) malloc(sizeof(Data));
+ do {
+ //store_32(&tmp->data1, prev->data1 + d1);
+ /********** Inadmissibility **********/
+ Data *prev = data.load(memory_order_acquire);
+ tmp->data1 = d1;
+ tmp->data2 = d2;
+ /********** Inadmissibility **********/
+ succ = data.compare_exchange_strong(prev, tmp,
+ memory_order_release, memory_order_relaxed);
/**
@Begin
- @Commit_point_check_define: true
- @Label: Read_Success_Point
+ @Commit_point_define_check: succ
+ @Label: Write_Success_Point
@End
*/
- res = cur_data_ptr->read();
- return res;
- }
+ } while (!succ);
+ //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+ return tmp;
+}
+
+
+void threadA(void *arg) {
+ write(1, 0);
+}
+
+void threadB(void *arg) {
+ write(0, 2);
+}
+void threadC(void *arg) {
+ write(2, 2);
+}
+
+void threadD(void *arg) {
+ Data *d = read();
+ printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
+}
+
+int user_main(int argc, char **argv) {
/**
@Begin
- @Interface: Write
- @Commit_point_set: Write_Success_Point
- @Action:
- @Code:
- __cur_data = new_data;
+ @Entry_point
@End
*/
- void write(Type *new_data) {
- while (true) {
- Type *prev = _data.load(memory_order_acquire);
- if (_data.compare_exchange_weak(prev, new_data,
- memory_order_release, memory_order_release)) {
- /**
- @Begin
- @Commit_point_check_define: __ATOMIC_RET__ == true
- @Label: Write_Success_Point
- @End
- */
- break;
- }
- }
- }
-};
+
+ thrd_t t1, t2, t3, t4;
+ Data *dataInit = (Data*) malloc(sizeof(Data));
+ dataInit->data1 = 0;
+ dataInit->data2 = 0;
+ atomic_init(&data, dataInit);
+
+ thrd_create(&t1, threadA, NULL);
+ thrd_create(&t2, threadB, NULL);
+ //thrd_create(&t3, threadC, NULL);
+ thrd_create(&t4, threadD, NULL);
+
+ thrd_join(t1);
+ thrd_join(t2);
+ //thrd_join(t3);
+ thrd_join(t4);
+
+ return 0;
+}
projects / cdsspec-compiler.git / blobdiff