--- /dev/null
+#ifndef __UNRELACY_H__
+#define __UNRELACY_H__
+
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <mutex>
+#include <condition_variable>
+
+#include <model-assert.h>
+#include <librace.h>
+
+#define $
+
+#define ASSERT(expr) MODEL_ASSERT(expr)
+#define RL_ASSERT(expr) MODEL_ASSERT(expr)
+
+#define RL_NEW new
+#define RL_DELETE(expr) delete expr
+
+#define mo_seqcst memory_order_relaxed
+#define mo_release memory_order_release
+#define mo_acquire memory_order_acquire
+#define mo_acq_rel memory_order_acq_rel
+#define mo_relaxed memory_order_relaxed
+
+namespace rl {
+
+ /* This 'useless' struct is declared just so we can use partial template
+ * specialization in our store and load functions. */
+ template <typename T, size_t n>
+ struct useless {
+ static void store(void *addr, T val);
+ static T load(const void *addr);
+ };
+
+ template <typename T>
+ struct useless<T, 1> {
+ static void store(void *addr, T val) { store_8(addr, (uint8_t)val); }
+ static T load(const void *addr) { return (T)load_8(addr); }
+ };
+
+ template <typename T>
+ struct useless<T, 2> {
+ static void store(void *addr, T val) { store_16(addr, (uint16_t)val); }
+ static T load(const void *addr) { return (T)load_16(addr); }
+ };
+
+ template <typename T>
+ struct useless<T, 4> {
+ static void store(void *addr, T val) { store_32(addr, (uint32_t)val); }
+ static T load(const void *addr) { return (T)load_32(addr); }
+ };
+
+ template <typename T>
+ struct useless<T, 8> {
+ static void store(void *addr, T val) { store_64(addr, (uint64_t)val); }
+ static T load(const void *addr) { return (T)load_64(addr); }
+ };
+
+ template <typename T>
+ struct var {
+ var() { useless<T, sizeof(T)>::store(&value, 0); }
+ var(T v) { useless<T, sizeof(T)>::store(&value, v); }
+ var(var const& r) {
+ value = r.value;
+ }
+ ~var() { }
+
+ void operator = (T v) { useless<T, sizeof(T)>::store(&value, v); }
+ T operator () () { return useless<T, sizeof(T)>::load(&value); }
+ void operator += (T v) {
+ useless<T, sizeof(T)>::store(&value,
+ useless<T, sizeof(T)>::load(&value) + v);
+ }
+ bool operator == (const struct var<T> v) const { return useless<T, sizeof(T)>::load(&value) == useless<T, sizeof(T)>::load(&v.value); }
+
+ T value;
+ };
+
+ class backoff_t
+ {
+ public:
+ typedef int debug_info_param;
+ void yield(debug_info_param info) { }
+ void yield() { }
+ };
+
+
+ typedef backoff_t backoff;
+ typedef backoff_t linear_backoff;
+ typedef backoff_t exp_backoff;
+
+}
+
+#endif /* __UNRELACY_H__ */
me->next.store(NULL, std::mo_relaxed );
me->gate.store(1, std::mo_relaxed );
+ /********** Inadmissible **********/
/** Run this in the -Y mode to expose the HB bug */
// publish my node as the new tail :
mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
rl::linear_backoff bo;
int my_gate = 1;
while (my_gate ) {
+ /********** Inadmissibility *********/
my_gate = me->gate.load(std::mo_acquire);
//if (my_gate == 0)
//printf("lock at gate!\n");
{
mcs_node * tail_was_me = me;
bool success;
+
+ /********** Inadmissible **********/
success = m_tail.compare_exchange_strong(
tail_was_me,NULL,std::mo_acq_rel);
/**
// (*2) - store to next must be done,
// so no locker can be viewing my node any more
+ /********** Inadmissible **********/
// let next guy in :
next->gate.store( 0, std::mo_release );
/**
include ../benchmarks.mk
-TESTNAME = rcu
+all: rcu
-all: $(TESTNAME)
-
-$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h
+rcp: rcu.cc
$(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
clean:
typedef struct Data {
int data1;
int data2;
- int data3;
} Data;
atomic<Data*> data;
@Begin
@Global_define:
@DeclareVar:
- int data1;
- int data2;
- int data3;
+ IntegerList *set;
@InitVar:
- data1 = 0;
- data2 = 0;
- data3 = 0;
+ 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
*/
@Begin
@Interface: Read
@Commit_point_set: Read_Success_Point
- //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
+ @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:
- data1 == __RET__->data1 &&
- data2 == __RET__->data2 &&
- data3 == __RET__->data3
+ _read(__RET__);
@End
*/
Data* read() {
+ /********** SPEC (sync) **********/
Data *res = data.load(memory_order_acquire);
//load_32(&res->data1);
/**
@Label: Read_Success_Point
@End
*/
- //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
return res;
}
@Begin
@Interface: Write
@Commit_point_set: Write_Success_Point
+ @ID: getID(d1, d2);
@Action:
- data1 += d1;
- data2 += d2;
- data3 += d3;
+ //model_print("Write_ID = %d\n", getID(d1, d2));
+ _write(d1, d2);
@End
*/
-Data* write(int d1, int d2, int d3) {
+Data* write(int d1, int d2) {
bool succ = false;
Data *tmp = (Data*) malloc(sizeof(Data));
- Data *prev = data.load(memory_order_acquire);
do {
//store_32(&tmp->data1, prev->data1 + d1);
- tmp->data1 = prev->data1 + d1;
- tmp->data2 = prev->data2 + d2;
- tmp->data3 = prev->data3 + d3;
+ /********** 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_acquire);
+ memory_order_release, memory_order_relaxed);
/**
@Begin
@Commit_point_define_check: succ
void threadA(void *arg) {
- write(1, 0, 0);
+ write(1, 0);
}
void threadB(void *arg) {
- write(0, 1, 0);
+ write(0, 2);
}
void threadC(void *arg) {
- write(0, 0, 1);
+ write(2, 2);
}
void threadD(void *arg) {
- Data *dataC = read();
+ Data *d = read();
+ printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
}
int user_main(int argc, char **argv) {
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_create(&t4, threadD, NULL);
thrd_join(t1);
thrd_join(t2);
//thrd_join(t3);
- //thrd_join(t4);
+ thrd_join(t4);
return 0;
}
concurrent-hashmap seqlock spsc-example spsc-queue-scfence \
treiber-stack
-DIRS := ms-queue concurrent-hashmap linuxrwlocks
+DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update
.PHONY: $(DIRS)
new File(homeDir + "/benchmark/ms-queue/main.c"),
new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
-// File[] srcRCU = { new File(homeDir
-// + "/benchmark/read-copy-update/rcu.cc") };
+ File[] srcRCU = { new File(homeDir
+ + "/benchmark/read-copy-update/rcu.cc") };
//
File[] srcTrylock = { new File(homeDir
+ "/benchmark/trylock/trylock.c") };
// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/testcase.c"),
// new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") };
//
-// File[] srcMCSLock = {
-// new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
-// new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
+ File[] srcMCSLock = {
+ new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
+ new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
//
// File[] srcSPSCQueue = {
// new File(homeDir + "/benchmark/spsc-bugfix/spsc-queue.cc"),
// File[][] sources = { srcLinuxRWLocks, srcMSQueue, srcRCU,
// srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
- File[][] sources = {srcLinuxRWLock1, srcLinuxRWLock2, srcLinuxRWLock3};
+ File[][] sources = {srcRCU};
// Compile all the benchmarks
for (int i = 0; i < sources.length; i++) {
CodeGenerator gen = new CodeGenerator(sources[i]);
projects / cdsspec-compiler.git / commitdiff