#include <stdlib.h>
#include <stdio.h>
-#include "librace.h"
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
-using namespace std;
+#include "librace.h"
/**
This is an example about how to specify the correctness of the
@Begin
@Global_define:
@DeclareVar:
- Data *_cur_data;
+ int data1;
+ int data2;
+ int data3;
@InitVar:
- _cur_data = NULL;
-
- @DefineFunc:
- bool equals(Data *ptr1, Data *ptr2) {
- if (ptr1->data1 == ptr2->data2
- && ptr1->data2 == ptr2->data2
- && ptr1->data3 == ptr2->data3) {
- return true;
- } else {
- return false;
- }
- }
-
+ data1 = 0;
+ data2 = 0;
+ data3 = 0;
@Happens_before:
Write -> Read
Write -> Write
@Begin
@Interface: Read
@Commit_point_set: Read_Success_Point
- @Action:
- Data *_Old_Data = _cur_data;
+ //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
@Post_check:
- equals(__RET__, _Old_Data)
+ data1 == __RET__->data1 &&
+ data2 == __RET__->data2 &&
+ data3 == __RET__->data3
@End
*/
Data* read() {
Data *res = data.load(memory_order_acquire);
+ //load_32(&res->data1);
/**
@Begin
@Commit_point_define_check: true
@Label: Read_Success_Point
@End
*/
+ //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
return res;
}
@Interface: Write
@Commit_point_set: Write_Success_Point
@Action:
- _cur_data = new_data;
+ data1 += d1;
+ data2 += d2;
+ data3 += d3;
@End
*/
-void write(Data *new_data) {
- while (true) {
- Data *prev = data.load(memory_order_relaxed);
- bool succ = data.compare_exchange_strong(prev, new_data,
- memory_order_release, memory_order_relaxed);
+Data* write(int d1, int d2, int d3) {
+ bool succ = false;
+ Data *tmp = (Data*) malloc(sizeof(Data));
+ do {
+ Data *prev = data.load(memory_order_acquire);
+ //store_32(&tmp->data1, prev->data1 + d1);
+ tmp->data1 = prev->data1 + d1;
+ tmp->data2 = prev->data2 + d2;
+ tmp->data3 = prev->data3 + d3;
+ succ = data.compare_exchange_strong(prev, tmp,
+ memory_order_acq_rel, memory_order_relaxed);
/**
@Begin
- @Commit_point_define_check: succ == true
+ @Commit_point_define_check: succ
@Label: Write_Success_Point
@End
*/
- if (succ) {
- break;
- }
- }
+ } while (!succ);
+ //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+ return tmp;
}
+
void threadA(void *arg) {
- Data *dataA = (Data*) malloc(sizeof(Data));
- dataA->data1 = 3;
- dataA->data2 = 2;
- dataA->data3 = 1;
- write(dataA);
+ write(1, 0, 0);
}
void threadB(void *arg) {
- Data *dataB = read();
- printf("ThreadB data1: %d\n", dataB->data1);
- printf("ThreadB data2: %d\n", dataB->data2);
- printf("ThreadB data3: %d\n", dataB->data3);
+ write(0, 1, 0);
+}
+
+void threadC(void *arg) {
+ write(0, 0, 1);
+}
+
+void threadD(void *arg) {
+ Data *dataC = read();
}
int user_main(int argc, char **argv) {
@End
*/
- thrd_t t1, t2;
- Data *data_init = (Data*) malloc(sizeof(Data));
- data_init->data1 = 1;
- data_init->data2 = 2;
- data_init->data3 = 3;
- write(data_init);
+ thrd_t t1, t2, t3, t4;
+ Data *dataInit = (Data*) malloc(sizeof(Data));
+ dataInit->data1 = 0;
+ dataInit->data2 = 0;
+ dataInit->data3 = 0;
+ atomic_init(&data, dataInit);
+ write(0, 0, 0);
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;
}