From: Peizhao Ou Date: Wed, 18 Nov 2015 01:12:13 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=17e78d57c56a42f19fde853278907d7bf4bb9bec edits --- diff --git a/benchmark/include/unrelacy.h b/benchmark/include/unrelacy.h new file mode 100644 index 0000000..729d76f --- /dev/null +++ b/benchmark/include/unrelacy.h @@ -0,0 +1,96 @@ +#ifndef __UNRELACY_H__ +#define __UNRELACY_H__ + +#include +#include +#include +#include +#include + +#include +#include + +#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 + struct useless { + static void store(void *addr, T val); + static T load(const void *addr); + }; + + template + struct useless { + 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 + struct useless { + 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 + struct useless { + 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 + struct useless { + 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 + struct var { + var() { useless::store(&value, 0); } + var(T v) { useless::store(&value, v); } + var(var const& r) { + value = r.value; + } + ~var() { } + + void operator = (T v) { useless::store(&value, v); } + T operator () () { return useless::load(&value); } + void operator += (T v) { + useless::store(&value, + useless::load(&value) + v); + } + bool operator == (const struct var v) const { return useless::load(&value) == useless::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__ */ diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h index bf49631..9f47812 100644 --- a/benchmark/mcs-lock/mcs-lock.h +++ b/benchmark/mcs-lock/mcs-lock.h @@ -76,6 +76,7 @@ public: 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); @@ -103,6 +104,7 @@ public: 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"); @@ -135,6 +137,8 @@ public: { mcs_node * tail_was_me = me; bool success; + + /********** Inadmissible **********/ success = m_tail.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel); /** @@ -164,6 +168,7 @@ public: // (*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 ); /** diff --git a/benchmark/read-copy-update/Makefile b/benchmark/read-copy-update/Makefile index 08941cf..1ddd57f 100644 --- a/benchmark/read-copy-update/Makefile +++ b/benchmark/read-copy-update/Makefile @@ -1,10 +1,8 @@ include ../benchmarks.mk -TESTNAME = rcu +all: rcu -all: $(TESTNAME) - -$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h +rcp: rcu.cc $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) clean: diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc index 5523882..2d517bc 100644 --- a/benchmark/read-copy-update/rcu.cc +++ b/benchmark/read-copy-update/rcu.cc @@ -21,7 +21,6 @@ typedef struct Data { int data1; int data2; - int data3; } Data; atomic data; @@ -30,16 +29,56 @@ atomic 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 */ @@ -47,14 +86,17 @@ atomic data; @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); /** @@ -63,7 +105,6 @@ Data* read() { @Label: Read_Success_Point @End */ - //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3); return res; } @@ -71,23 +112,24 @@ Data* read() { @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 @@ -101,19 +143,20 @@ Data* write(int d1, int d2, int d3) { 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) { @@ -127,19 +170,17 @@ 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; } diff --git a/output/Makefile b/output/Makefile index c232475..7877016 100644 --- a/output/Makefile +++ b/output/Makefile @@ -3,7 +3,7 @@ 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) diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index 4e74668..c75fd81 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -312,8 +312,8 @@ public class CodeGenerator { 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") }; @@ -324,9 +324,9 @@ public class CodeGenerator { // 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"), @@ -340,7 +340,7 @@ public class CodeGenerator { // 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]);