edits

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 010704c61985e31280af3668a32b340acd433750..b4f63171fde4fda413384f3f7eeae90f816fcdab 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -118,7 +118,7 @@ void push(Deque *q, int x) {
                resize(q);
                // CDSSpec can actually detect the same bug if we avoid the UL error
                //Bug in paper...should have next line...
                resize(q);
                // CDSSpec can actually detect the same bug if we avoid the UL error
                //Bug in paper...should have next line...

-               //a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+               a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);

                /**
                        //@Begin
                        @Commit_point_define_check: true
                /**
                        //@Begin
                        @Commit_point_define_check: true

diff --git a/output/Makefile b/output/Makefile
index a5b333b3b7cf1045974c43b57efdc3fa0a7e1464..fc544402b7c2c4bcd7c6681dfbc2437b431822e8 100644 (file)
--- a/output/Makefile
+++ b/output/Makefile
@@ -4,7 +4,7 @@
        treiber-stack
 
 DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update \
        treiber-stack
 
 DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update \

-       chase-lev-deque-bugfix spsc-bugfix mpmc-queue
+       chase-lev-deque-bugfix spsc-bugfix mpmc-queue seqlock

 
 .PHONY: $(DIRS)
 
 
 .PHONY: $(DIRS)
 

diff --git a/output/benchmarks.mk b/output/benchmarks.mk
index 20a76d8b0e92f77af99a82e18fa893823b984b47..e7a873600ea6267508bdce2772f0ae9feabe2ad7 100644 (file)
--- a/output/benchmarks.mk
+++ b/output/benchmarks.mk
@@ -12,7 +12,7 @@ BASE = $(HOME)/model-checker-priv/model-checker-priv
 INCLUDE = -I$(BASE)/include -I../include -I$(BASE)/spec-analysis -I$(BASE)
 
 # C preprocessor flags
 INCLUDE = -I$(BASE)/include -I../include -I$(BASE)/spec-analysis -I$(BASE)
 
 # C preprocessor flags

-CPPFLAGS += $(INCLUDE) -g
+CPPFLAGS += $(INCLUDE) -O3

 
 # C++ compiler flags
 CXXFLAGS += $(CPPFLAGS)
 
 # C++ compiler flags
 CXXFLAGS += $(CPPFLAGS)

diff --git a/output/chase-lev-deque-bugfix/deque.c b/output/chase-lev-deque-bugfix/deque.c
index 15ffe0f9aae0a5ee81fcadbc9075198483e51f7b..68eab074bb24c303aee51e4698d04bfde2be89db 100644 (file)
--- a/output/chase-lev-deque-bugfix/deque.c
+++ b/output/chase-lev-deque-bugfix/deque.c
@@ -153,7 +153,8 @@ void __wrapper__push(Deque * q, int x) {
        Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1)  {
                resize(q);
        Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1)  {
                resize(q);

-                                                               
+                                               a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+               

        }
        int size = atomic_load_explicit(&a->size, memory_order_relaxed);
 
        }
        int size = atomic_load_explicit(&a->size, memory_order_relaxed);