add subdirectory for tests

diff --git a/libcdsTest/ms-queue/.intrusive_msqueue_hp.cc b/libcdsTest/ms-queue/.intrusive_msqueue_hp.cc
new file mode 100644 (file)
index 0000000..877f545
--- /dev/null
+++ b/libcdsTest/ms-queue/.intrusive_msqueue_hp.cc
@@ -0,0 +1,125 @@
+#include "test_intrusive_msqueue.h"
+
+#include <stdio.h>
+#include <cds/init.h>
+#include <cds/gc/hp.h>
+#include <cds/intrusive/msqueue.h>
+#include <vector>
+
+namespace ci = cds::intrusive;
+typedef cds::gc::HP gc_type;
+
+typedef cds_test::intrusive_msqueue base_class;
+typedef typename base_class::base_hook_item< ci::msqueue::node<gc_type>> base_item_type;
+typedef typename base_class::member_hook_item< ci::msqueue::node<gc_type>> member_item_type;
+
+typedef cds_test::intrusive_msqueue::mock_disposer mock_disposer;
+
+template <typename Queue, typename Data>
+void test( Queue& q, Data& arr )
+{
+    typedef typename Queue::value_type value_type;
+    size_t nSize = arr.size();
+
+    value_type * pv;
+    for ( size_t i = 0; i < nSize; ++i )
+       arr[i].nVal = static_cast<int>(i);
+
+    assert(q.empty());
+    assert(q.size() == 0);
+
+    // pop from empty queue
+    pv = q.pop();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+    pv =q.dequeue();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+    // push/pop test
+    for ( size_t i = 0; i < nSize; ++i ) {
+       if ( i & 1 )
+           q.push( arr[i] );
+       else
+           q.enqueue( arr[i] );
+       assert( !q.empty());
+       assert(q.size() == i+1);
+    }
+
+    for ( size_t i = 0; i < nSize; ++i ) {
+       assert( !q.empty());
+       assert( q.size() == nSize - i );
+       if ( i & 1 )
+           pv = q.pop();
+       else
+           pv = q.dequeue();
+       assert( pv != nullptr );
+       assert( pv->nVal == i);
+    }
+    assert( q.empty());
+    assert( q.size() == 0 );
+
+    Queue::gc::scan();
+    --nSize; // last element of array is in queue yet as a dummy item
+    for ( size_t i = 0; i < nSize; ++i ) {
+       assert( arr[i].nDisposeCount == 1 );
+    }
+    assert( arr[nSize].nDisposeCount == 0 );
+
+    // clear test
+    for ( size_t i = 0; i < nSize; ++i )
+       q.push( arr[i] );
+
+    assert( !q.empty());
+    assert( q.size() == nSize );
+
+    q.clear();
+    assert( q.empty());
+    assert( q.size() == 0 );
+
+    Queue::gc::scan();
+    for ( size_t i = 0; i < nSize - 1; ++i ) {
+       printf("nDisCount (2): %d, (i) %lu\n",  arr[i].nDisposeCount, i );
+    }
+    printf("nDisCount: (1) %d\n",  arr[nSize - 1].nDisposeCount ); // this element is in the queue yet
+    assert( arr[nSize].nDisposeCount == 1 );
+}
+
+int main () {
+       cds::Initialize();
+
+       {
+               typedef ci::MSQueue< gc_type, base_item_type > queue_type;      
+               cds::gc::hp::GarbageCollector::Construct( queue_type::c_nHazardPtrCount, 1, 16 );
+               cds::threading::Manager::attachThread();
+
+               {
+                       typedef cds::intrusive::MSQueue< gc_type, base_item_type,
+                           typename ci::msqueue::make_traits<
+                               ci::opt::disposer< mock_disposer >
+                               , cds::opt::item_counter< cds::atomicity::item_counter >
+                               , ci::opt::hook< ci::msqueue::base_hook< ci::opt::gc<gc_type>>>
+                           >::type
+                       > test_queue;
+
+                       std::vector<base_item_type> arr;
+                       arr.resize(5);
+                       printf("test start\n");
+                       {
+                               test_queue q;
+                               test(q, arr);
+                       }
+                       printf("test end\n");
+
+//                     gc_type::scan();
+//                     check_array( arr );
+
+               }
+
+       }
+
+       cds::Terminate();
+}

diff --git a/libcdsTest/ms-queue/Makefile b/libcdsTest/ms-queue/Makefile
new file mode 100644 (file)
index 0000000..8df2ca5
--- /dev/null
+++ b/libcdsTest/ms-queue/Makefile
@@ -0,0 +1,15 @@
+all: intrusive_msqueue_hp.o
+
+#%.o : %.cc 
+#      $(CXX) -c $@
+
+CFLAGS=-I. -I /scratch/benchmarks/libcds -std=c++11
+
+CDSDIR=/scratch/benchmarks/libcds/build-release/bin
+CDSLIB=-lcds_d -lpthread
+
+intrusive_msqueue_hp.o: intrusive_msqueue_hp.cc
+       $(CXX) -o msqueue intrusive_msqueue_hp.cc $(CFLAGS) -L $(CDSDIR) $(CDSLIB)
+
+clean:
+       rm -f *.o

diff --git a/libcdsTest/ms-queue/intrusive_msqueue_hp.cc b/libcdsTest/ms-queue/intrusive_msqueue_hp.cc
new file mode 100644 (file)
index 0000000..176ba50
--- /dev/null
+++ b/libcdsTest/ms-queue/intrusive_msqueue_hp.cc
@@ -0,0 +1,174 @@
+#include "test_intrusive_msqueue.h"
+
+#include <stdio.h>
+#include <cds/init.h>
+#include <cds/gc/hp.h>
+#include <cds/intrusive/msqueue.h>
+#include <vector>
+
+#define NDEBUG         // disable assert()
+#include <assert.h>
+#include <atomic>
+
+namespace ci = cds::intrusive;
+typedef cds::gc::HP gc_type;
+
+typedef cds_test::intrusive_msqueue base_class;
+typedef typename base_class::base_hook_item< ci::msqueue::node<gc_type>> base_item_type;
+typedef typename base_class::member_hook_item< ci::msqueue::node<gc_type>> member_item_type;
+
+typedef cds_test::intrusive_msqueue::mock_disposer mock_disposer;
+
+template <typename Queue, typename Data>
+void test_enqueue( Queue& q, Data& arr )
+{
+    typedef typename Queue::value_type value_type;
+    size_t nSize = arr.size();
+
+    value_type * pv;
+    for ( size_t i = 0; i < nSize; ++i )
+       arr[i].nVal = static_cast<int>(i);
+
+    assert(q.empty());
+    assert(q.size() == 0);
+
+    // pop from empty queue
+//    pv = q.pop();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+//    pv = q.dequeue();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+    for ( size_t i = 0; i < nSize; ++i ) {
+       if ( i & 1 )
+           q.push( arr[i] );
+       else
+           q.enqueue( arr[i] );
+       assert( !q.empty());
+       assert(q.size() == i+1);
+    }
+}
+
+
+template <typename Queue, typename Data>
+void test_dequeue( Queue& q, Data& arr )
+{
+    typedef typename Queue::value_type value_type;
+    size_t nSize = arr.size();
+
+    value_type * pv;
+/*
+    for ( size_t i = 0; i < nSize; ++i )
+       arr[i].nVal = static_cast<int>(i);
+
+    assert(q.empty());
+    assert(q.size() == 0);
+
+    // pop from empty queue
+    pv = q.pop();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+    pv = q.dequeue();
+    assert( pv == nullptr );
+    assert( q.empty());
+    assert(q.size() == 0);
+
+    // push/pop test
+    for ( size_t i = 0; i < nSize; ++i ) {
+       if ( i & 1 )
+           q.push( arr[i] );
+       else
+           q.enqueue( arr[i] );
+       assert( !q.empty());
+       assert(q.size() == i+1);
+    }
+*/
+
+    for ( size_t i = 0; i < nSize; ++i ) {
+       assert( !q.empty());
+       assert( q.size() == nSize - i );
+       if ( i & 1 )
+           pv = q.pop();
+       else
+           pv = q.dequeue();
+       assert( pv != nullptr );
+       assert( pv->nVal == i);
+    }
+    assert( q.empty());
+    assert( q.size() == 0 );
+
+/*
+    Queue::gc::scan();
+    --nSize; // last element of array is in queue yet as a dummy item
+    for ( size_t i = 0; i < nSize; ++i ) {
+       assert( arr[i].nDisposeCount == 1 );
+    }
+    assert( arr[nSize].nDisposeCount == 0 );
+
+    // clear test
+    for ( size_t i = 0; i < nSize; ++i )
+       q.push( arr[i] );
+
+    assert( !q.empty());
+    assert( q.size() == nSize );
+
+    q.clear();
+    assert( q.empty());
+    assert( q.size() == 0 );
+
+    Queue::gc::scan();
+    for ( size_t i = 0; i < nSize - 1; ++i ) {
+       printf("nDisCount (2): %d, (i) %lu\n",  arr[i].nDisposeCount, i );
+    }
+    printf("nDisCount: (1) %d\n",  arr[nSize - 1].nDisposeCount ); // this element is in the queue yet
+    assert( arr[nSize].nDisposeCount == 1 );
+*/
+
+}
+
+int main () {
+       cds::Initialize();
+
+       {
+               typedef ci::MSQueue< gc_type, base_item_type > queue_type;      
+               cds::gc::hp::GarbageCollector::Construct( queue_type::c_nHazardPtrCount, 1, 16 );
+               cds::threading::Manager::attachThread();
+
+               {
+                       typedef cds::intrusive::MSQueue< gc_type, base_item_type,
+                           typename ci::msqueue::make_traits<
+                               ci::opt::disposer< mock_disposer >
+                               , cds::opt::item_counter< cds::atomicity::item_counter >
+                               , ci::opt::hook< ci::msqueue::base_hook< ci::opt::gc<gc_type>>>
+                           >::type
+                       > test_queue;
+
+                       std::vector<base_item_type> arr;
+                       arr.resize(5);
+                       printf("test start\n");
+                       {
+                               std::atomic<int> x;
+                               atomic_store_explicit(&x, 0xaaa, std::memory_order_seq_cst);
+                               test_queue q;
+                               test_enqueue(q, arr);
+                               atomic_store_explicit(&x, 0xccc, std::memory_order_seq_cst);
+                               test_dequeue(q, arr);
+                               atomic_store_explicit(&x, 0xbbb, std::memory_order_seq_cst);
+                       }
+                       printf("test end\n");
+
+//                     gc_type::scan();
+//                     check_array( arr );
+
+               }
+
+       }
+
+       cds::Terminate();
+}

diff --git a/libcdsTest/ms-queue/msqueue b/libcdsTest/ms-queue/msqueue
new file mode 100755 (executable)
index 0000000..ebafe1e
Binary files /dev/null and b/libcdsTest/ms-queue/msqueue differ

diff --git a/libcdsTest/ms-queue/msqueue2 b/libcdsTest/ms-queue/msqueue2
new file mode 100755 (executable)
index 0000000..ded5d2a
Binary files /dev/null and b/libcdsTest/ms-queue/msqueue2 differ

diff --git a/libcdsTest/ms-queue/other b/libcdsTest/ms-queue/other
new file mode 100755 (executable)
index 0000000..e6da92d
Binary files /dev/null and b/libcdsTest/ms-queue/other differ

diff --git a/libcdsTest/ms-queue/script.sh b/libcdsTest/ms-queue/script.sh
new file mode 100755 (executable)
index 0000000..9aa7253
--- /dev/null
+++ b/libcdsTest/ms-queue/script.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+clang++ -o msqueue2 -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so  intrusive_msqueue_hp.cc -I. -I /scratch/benchmarks/libcds -g -std=c++11 -L /scratch/random-fuzzer -lmodel -L /scratch/benchmarks/libcds/build-release/bin -lcds_d -lpthread

diff --git a/libcdsTest/ms-queue/test_intrusive_msqueue.h b/libcdsTest/ms-queue/test_intrusive_msqueue.h
new file mode 100644 (file)
index 0000000..8890cd3
--- /dev/null
+++ b/libcdsTest/ms-queue/test_intrusive_msqueue.h
@@ -0,0 +1,60 @@
+// Copyright (c) 2006-2018 Maxim Khizhinsky
+//
+// Distributed under the Boost Software License, Version 1.0. (See accompanying
+// file LICENSE or copy at http://www.boost.org/LICENSE_1_0.txt)
+
+#ifndef CDSUNIT_QUEUE_TEST_INTRUSIVE_MSQUEUE_H
+#define CDSUNIT_QUEUE_TEST_INTRUSIVE_MSQUEUE_H
+
+namespace cds_test {
+
+    class intrusive_msqueue
+    {
+    public:
+        template <typename Base>
+        struct base_hook_item : public Base
+        {
+            int nVal;
+            int nDisposeCount;
+
+            base_hook_item()
+                : nDisposeCount( 0 )
+            {}
+
+            base_hook_item( base_hook_item const& s)
+                : nVal( s.nVal )
+                , nDisposeCount( s.nDisposeCount )
+            {}
+        };
+
+        template <typename Member>
+        struct member_hook_item
+        {
+            int nVal;
+            int nDisposeCount;
+            Member hMember;
+
+            member_hook_item()
+                : nDisposeCount( 0 )
+            {}
+
+            member_hook_item( member_hook_item const& s )
+                : nVal( s.nVal )
+                , nDisposeCount( s.nDisposeCount )
+            {}
+        };
+
+        struct mock_disposer
+        {
+            template <typename T>
+            void operator ()( T * p )
+            {
+                ++p->nDisposeCount;
+            }
+        };
+
+    };
+
+} // namespace cds_test
+
+#endif // CDSUNIT_QUEUE_TEST_INTRUSIVE_MSQUEUE_H

diff --git a/libcdsTest/ms-queue/tmp b/libcdsTest/ms-queue/tmp
new file mode 100644 (file)
index 0000000..1dacb27
--- /dev/null
+++ b/libcdsTest/ms-queue/tmp
@@ -0,0 +1,242 @@
+key_delete is called
+has write to location: 0x60c1e0 values: 1 
+has write to location: 0x1a82928 values: 1a82a10 1a82a20 1a82a30 1a82a40 1a82a50 
+has write to location: 0x1a82980 values: 1 2 3 4 5 6 7 8 9 a b c d e f 10 11 
+has write to location: 0x1a829e0 values: 7f74888ecf28 0 1a82b10 0 1a82b20 0 1a82b30 0 1a82b40 0 7f74888ecf28 0 1a82b20 0 1a82b20 0 1a82b40 0 1a82b40 0 0 0 
+has write to location: 0x1a829f0 values: 1a82b10 0 1a82b10 0 1a82b30 0 1a82b30 0 1a82b50 0 1a82b50 0 
+has write to location: 0x1a82b10 values: 0 1a82b20 
+has write to location: 0x1a82b20 values: 0 1a82b30 
+has write to location: 0x1a82b30 values: 0 1a82b40 
+has write to location: 0x1a82b40 values: 0 1a82b50 
+has write to location: 0x1a82b50 values: 0 
+has write to location: 0x7f74888ecea8 values: 1a82b10 1a82b20 1a82b30 1a82b40 1a82b50 0 
+has write to location: 0x7f74888ecee8 values: 1a82b10 1a82b20 1a82b30 1a82b40 1a82b50 0 
+has write to location: 0x7f74888ecf28 values: 0 1a82b10 
+has write to location: 0x7f74888ecf68 values: 1 2 3 4 5 4 3 2 1 0 
+has write to location: 0x7f74888ecf78 values: aaa ccc bbb 
+-----------------------------------------
+location: 0x60c1e0: 
+0    0    uninitialized   relaxed        0x60c1e0   0                       ( 0)
+location: 0x7f74888ecee8: 
+0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
+location: 0x1a82980: 
+0    0    uninitialized   relaxed       0x1a82980   0                       ( 0)
+location: 0x7f74888ecee8: 
+0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
+location: 0x7f74888ecf28: 
+9    1    atomic write    release  0x7f74888ecf28   0                       ( 0,  9)
+location: 0x7f74888ecf28: 
+9    1    atomic write    release  0x7f74888ecf28   0                       ( 0,  9)
+location: 0x7f74888ecf68: 
+0    0    uninitialized   relaxed  0x7f74888ecf68   0                       ( 0)
+location: 0x7f74888ecee8: 
+0    0    uninitialized   relaxed  0x7f74888ecee8   0x7f74888ecf28          ( 0)
+location: 0x7f74888ecee8: 
+17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
+location: 0x1a82980: 
+12   1    atomic rmw      acq_rel       0x1a82980   0                   0   ( 0, 12)
+location: 0x7f74888ecee8: 
+17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
+location: 0x1a82b10: 
+3    1    atomic write    release       0x1a82b10   0                       ( 0,  3)
+location: 0x1a82b10: 
+3    1    atomic write    release       0x1a82b10   0                       ( 0,  3)
+location: 0x7f74888ecf68: 
+16   1    atomic rmw      relaxed  0x7f74888ecf68   0                   0   ( 0, 16)
+location: 0x7f74888ecee8: 
+17   1    atomic rmw      release  0x7f74888ecee8   0x7f74888ecf28      0   ( 0, 17)
+location: 0x7f74888ecee8: 
+26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
+location: 0x1a82980: 
+21   1    atomic rmw      acq_rel       0x1a82980   0x1                 12  ( 0, 21)
+location: 0x7f74888ecee8: 
+26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
+location: 0x1a82b20: 
+4    1    atomic write    release       0x1a82b20   0                       ( 0,  4)
+location: 0x1a82b20: 
+4    1    atomic write    release       0x1a82b20   0                       ( 0,  4)
+location: 0x7f74888ecf68: 
+25   1    atomic rmw      relaxed  0x7f74888ecf68   0x1                 16  ( 0, 25)
+location: 0x7f74888ecee8: 
+26   1    atomic rmw      release  0x7f74888ecee8   0x1a82b10           17  ( 0, 26)
+location: 0x7f74888ecee8: 
+35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
+location: 0x1a82980: 
+30   1    atomic rmw      acq_rel       0x1a82980   0x2                 21  ( 0, 30)
+location: 0x7f74888ecee8: 
+35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
+location: 0x1a82b30: 
+5    1    atomic write    release       0x1a82b30   0                       ( 0,  5)
+location: 0x1a82b30: 
+5    1    atomic write    release       0x1a82b30   0                       ( 0,  5)
+location: 0x7f74888ecf68: 
+34   1    atomic rmw      relaxed  0x7f74888ecf68   0x2                 25  ( 0, 34)
+location: 0x7f74888ecee8: 
+35   1    atomic rmw      release  0x7f74888ecee8   0x1a82b20           26  ( 0, 35)
+location: 0x7f74888ecee8: 
+44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
+location: 0x1a82980: 
+39   1    atomic rmw      acq_rel       0x1a82980   0x3                 30  ( 0, 39)
+location: 0x7f74888ecee8: 
+44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
+location: 0x1a82b40: 
+6    1    atomic write    release       0x1a82b40   0                       ( 0,  6)
+location: 0x1a82b40: 
+6    1    atomic write    release       0x1a82b40   0                       ( 0,  6)
+location: 0x7f74888ecf68: 
+43   1    atomic rmw      relaxed  0x7f74888ecf68   0x3                 34  ( 0, 43)
+location: 0x7f74888ecee8: 
+44   1    atomic rmw      release  0x7f74888ecee8   0x1a82b30           35  ( 0, 44)
+location: 0x7f74888ecea8: 
+0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
+location: 0x1a82980: 
+48   1    atomic rmw      acq_rel       0x1a82980   0x4                 39  ( 0, 48)
+location: 0x7f74888ecea8: 
+0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
+location: 0x7f74888ecf28: 
+15   1    atomic rmw      release  0x7f74888ecf28   0                   9   ( 0, 15)
+location: 0x1a82980: 
+58   1    atomic rmw      acq_rel       0x1a82980   0x5                 48  ( 0, 58)
+location: 0x7f74888ecf28: 
+15   1    atomic rmw      release  0x7f74888ecf28   0                   9   ( 0, 15)
+location: 0x7f74888ecea8: 
+0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x7f74888ecea8: 
+0    0    uninitialized   relaxed  0x7f74888ecea8   0x7f74888ecf28          ( 0)
+location: 0x7f74888ecf68: 
+52   1    atomic rmw      relaxed  0x7f74888ecf68   0x4                 43  ( 0, 52)
+location: 0x7f74888ecea8: 
+66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
+location: 0x1a82980: 
+62   1    atomic rmw      acq_rel       0x1a82980   0x6                 58  ( 0, 62)
+location: 0x7f74888ecea8: 
+66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
+location: 0x1a82b10: 
+24   1    atomic rmw      release       0x1a82b10   0                   3   ( 0, 24)
+location: 0x1a82980: 
+72   1    atomic rmw      acq_rel       0x1a82980   0x7                 62  ( 0, 72)
+location: 0x1a82b10: 
+24   1    atomic rmw      release       0x1a82b10   0                   3   ( 0, 24)
+location: 0x7f74888ecea8: 
+66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x7f74888ecea8: 
+66   1    atomic rmw      acquire  0x7f74888ecea8   0x7f74888ecf28      0   ( 0, 66)
+location: 0x7f74888ecf68: 
+67   1    atomic rmw      relaxed  0x7f74888ecf68   0x5                 52  ( 0, 67)
+location: 0x1a82928: 
+0    0    uninitialized   relaxed       0x1a82928   0x1a82a00               ( 0)
+location: 0x7f74888ecea8: 
+80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
+location: 0x1a82980: 
+76   1    atomic rmw      acq_rel       0x1a82980   0x8                 72  ( 0, 76)
+location: 0x7f74888ecea8: 
+80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
+location: 0x1a82b20: 
+33   1    atomic rmw      release       0x1a82b20   0                   4   ( 0, 33)
+location: 0x1a82980: 
+88   1    atomic rmw      acq_rel       0x1a82980   0x9                 76  ( 0, 88)
+location: 0x1a82b20: 
+33   1    atomic rmw      release       0x1a82b20   0                   4   ( 0, 33)
+location: 0x7f74888ecea8: 
+80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x7f74888ecea8: 
+80   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b10           66  ( 0, 80)
+location: 0x7f74888ecf68: 
+81   1    atomic rmw      relaxed  0x7f74888ecf68   0x4                 67  ( 0, 81)
+location: 0x1a82928: 
+83   1    atomic write    relaxed       0x1a82928   0x1a82a10               ( 0, 83)
+location: 0x7f74888ecea8: 
+96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
+location: 0x1a82980: 
+92   1    atomic rmw      acq_rel       0x1a82980   0xa                 88  ( 0, 92)
+location: 0x7f74888ecea8: 
+96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
+location: 0x1a82b30: 
+42   1    atomic rmw      release       0x1a82b30   0                   5   ( 0, 42)
+location: 0x1a82980: 
+104  1    atomic rmw      acq_rel       0x1a82980   0xb                 92  ( 0, 104)
+location: 0x1a82b30: 
+42   1    atomic rmw      release       0x1a82b30   0                   5   ( 0, 42)
+location: 0x7f74888ecea8: 
+96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x7f74888ecea8: 
+96   1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b20           80  ( 0, 96)
+location: 0x7f74888ecf68: 
+97   1    atomic rmw      relaxed  0x7f74888ecf68   0x3                 81  ( 0, 97)
+location: 0x1a82928: 
+99   1    atomic write    relaxed       0x1a82928   0x1a82a20               ( 0, 99)
+location: 0x7f74888ecea8: 
+112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
+location: 0x1a82980: 
+108  1    atomic rmw      acq_rel       0x1a82980   0xc                 104 ( 0, 108)
+location: 0x7f74888ecea8: 
+112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
+location: 0x1a82b40: 
+51   1    atomic rmw      release       0x1a82b40   0                   6   ( 0, 51)
+location: 0x1a82980: 
+120  1    atomic rmw      acq_rel       0x1a82980   0xd                 108 ( 0, 120)
+location: 0x1a82b40: 
+51   1    atomic rmw      release       0x1a82b40   0                   6   ( 0, 51)
+location: 0x7f74888ecea8: 
+112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x7f74888ecea8: 
+112  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b30           96  ( 0, 112)
+location: 0x7f74888ecf68: 
+113  1    atomic rmw      relaxed  0x7f74888ecf68   0x2                 97  ( 0, 113)
+location: 0x1a82928: 
+115  1    atomic write    relaxed       0x1a82928   0x1a82a30               ( 0, 115)
+location: 0x7f74888ecea8: 
+128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
+location: 0x1a82980: 
+124  1    atomic rmw      acq_rel       0x1a82980   0xe                 120 ( 0, 124)
+location: 0x7f74888ecea8: 
+128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
+location: 0x1a82b50: 
+7    1    atomic write    release       0x1a82b50   0                       ( 0,  7)
+location: 0x1a82980: 
+137  1    atomic rmw      acq_rel       0x1a82980   0xf                 124 ( 0, 137)
+location: 0x1a82b50: 
+7    1    atomic write    release       0x1a82b50   0                       ( 0,  7)
+location: 0x7f74888ecea8: 
+128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
+location: 0x7f74888ecea8: 
+128  1    atomic rmw      acquire  0x7f74888ecea8   0x1a82b40           112 ( 0, 128)
+location: 0x7f74888ecee8: 
+53   1    atomic rmw      release  0x7f74888ecee8   0x1a82b40           44  ( 0, 53)
+location: 0x1a82928: 
+131  1    atomic write    relaxed       0x1a82928   0x1a82a40               ( 0, 131)
+Program output from execution 1:
+---- BEGIN PROGRAM OUTPUT ----
+test start
+libcds - enqueue node m_pTail loc: 0x7f74888ecee8
+libcds - enqueue node m_pTail loc: 0x7f74888ecee8
+libcds - enqueue node m_pTail loc: 0x7f74888ecee8
+libcds - enqueue node m_pTail loc: 0x7f74888ecee8
+libcds - enqueue node m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+libcds - do_dequeue hode m_pHead loc: 0x7f74888ecea8
+libcds - do_dequeue hode m_pTail loc: 0x7f74888ecee8
+test end
+---- END PROGRAM OUTPUT   ----
+
+ecee8: ecf28, 1a82b10, 1a82b20, 1a82b30, 1a82b40, 1a82b50
+

diff --git a/pthread_test/CDSPass/addr-satcycle.cc b/pthread_test/CDSPass/addr-satcycle.cc
new file mode 100755 (executable)
index 0000000..84aa83d
Binary files /dev/null and b/pthread_test/CDSPass/addr-satcycle.cc differ

diff --git a/pthread_test/CDSPass/bug1.cc b/pthread_test/CDSPass/bug1.cc
new file mode 100755 (executable)
index 0000000..fe715a6
Binary files /dev/null and b/pthread_test/CDSPass/bug1.cc differ

diff --git a/pthread_test/CDSPass/compile.sh b/pthread_test/CDSPass/compile.sh
new file mode 100755 (executable)
index 0000000..56e324e
--- /dev/null
+++ b/pthread_test/CDSPass/compile.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+# C test cases
+# clang -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -c -I/scratch/random-fuzzer/include/  /scratch/random-fuzzer/test/userprog.c
+
+# gcc -o userprog userprog.o -L/scratch/random-fuzzer -lmodel
+
+
+DIR=/scratch/random-fuzzer/pthread_test/CDSPass/dummy
+
+export LD_LIBRARY_PATH=/scratch/random-fuzzer
+
+# compile with CDSPass 
+if [ "$2" != "" ]; then # C++
+  clang++ -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -g -o $DIR/$1.o -I /scratch/random-fuzzer/include -L/scratch/random-fuzzer -lmodel $1
+else # C
+  clang -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -o $DIR/$1.o -I/scratch/random-fuzzer/include/ -L/scratch/random-fuzzer -lmodel $1
+fi

diff --git a/pthread_test/CDSPass/condvar.cc b/pthread_test/CDSPass/condvar.cc
new file mode 100755 (executable)
index 0000000..f4f111b
Binary files /dev/null and b/pthread_test/CDSPass/condvar.cc differ

diff --git a/pthread_test/CDSPass/deadlock.cc b/pthread_test/CDSPass/deadlock.cc
new file mode 100755 (executable)
index 0000000..76a9376
Binary files /dev/null and b/pthread_test/CDSPass/deadlock.cc differ

diff --git a/pthread_test/CDSPass/insanesync.cc b/pthread_test/CDSPass/insanesync.cc
new file mode 100755 (executable)
index 0000000..00bb40d
Binary files /dev/null and b/pthread_test/CDSPass/insanesync.cc differ

diff --git a/pthread_test/CDSPass/iriw.cc b/pthread_test/CDSPass/iriw.cc
new file mode 100755 (executable)
index 0000000..8042a13
Binary files /dev/null and b/pthread_test/CDSPass/iriw.cc differ

diff --git a/pthread_test/CDSPass/iriw_wildcard.cc b/pthread_test/CDSPass/iriw_wildcard.cc
new file mode 100755 (executable)
index 0000000..1b17a2a
Binary files /dev/null and b/pthread_test/CDSPass/iriw_wildcard.cc differ

diff --git a/pthread_test/CDSPass/mo-satcycle.cc b/pthread_test/CDSPass/mo-satcycle.cc
new file mode 100755 (executable)
index 0000000..8093885
Binary files /dev/null and b/pthread_test/CDSPass/mo-satcycle.cc differ

diff --git a/pthread_test/CDSPass/mutex_test.cc b/pthread_test/CDSPass/mutex_test.cc
new file mode 100755 (executable)
index 0000000..2c605c0
Binary files /dev/null and b/pthread_test/CDSPass/mutex_test.cc differ

diff --git a/pthread_test/CDSPass/pthread_mutex_test.cc b/pthread_test/CDSPass/pthread_mutex_test.cc
new file mode 100755 (executable)
index 0000000..ebda328
Binary files /dev/null and b/pthread_test/CDSPass/pthread_mutex_test.cc differ

diff --git a/pthread_test/CDSPass/uninit b/pthread_test/CDSPass/uninit
new file mode 100755 (executable)
index 0000000..f6b682f
Binary files /dev/null and b/pthread_test/CDSPass/uninit differ

diff --git a/pthread_test/CDSPass/uninit.cc b/pthread_test/CDSPass/uninit.cc
new file mode 100755 (executable)
index 0000000..f6b682f
Binary files /dev/null and b/pthread_test/CDSPass/uninit.cc differ

diff --git a/pthread_test/addr-satcycle.cc b/pthread_test/addr-satcycle.cc
new file mode 100644 (file)
index 0000000..a3d970b
--- /dev/null
+++ b/pthread_test/addr-satcycle.cc
@@ -0,0 +1,69 @@
+/**
+ * @file addr-satcycle.cc
+ * @brief Address-based satisfaction cycle test
+ *
+ * This program has a peculiar behavior which is technically legal under the
+ * current C++ memory model but which is a result of a type of satisfaction
+ * cycle. We use this as justification for part of our modifications to the
+ * memory model when proving our model-checker's correctness.
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+
+#include "model-assert.h"
+
+using namespace std;
+
+atomic_int x[2], idx, y;
+
+int r1, r2, r3; /* "local" variables */
+
+static void *a(void *obj)
+{
+       r1 = idx.load(memory_order_relaxed);
+       x[r1].store(0, memory_order_relaxed);
+
+       /* Key point: can we guarantee that &x[0] == &x[r1]? */
+       r2 = x[0].load(memory_order_relaxed);
+       y.store(r2);
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       r3 = y.load(memory_order_relaxed);
+       idx.store(r3, memory_order_relaxed);
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2;
+
+       atomic_init(&x[0], 1);
+       atomic_init(&idx, 0);
+       atomic_init(&y, 0);
+
+       printf("Main thread: creating 2 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       printf("Main thread is finished\n");
+
+       printf("r1 = %d\n", r1);
+       printf("r2 = %d\n", r2);
+       printf("r3 = %d\n", r3);
+
+       /*
+        * This condition should not be hit because it only occurs under a
+        * satisfaction cycle
+        */
+       bool cycle = (r1 == 1 && r2 == 1 && r3 == 1);
+       MODEL_ASSERT(!cycle);
+
+       return 0;
+}

diff --git a/pthread_test/bug1.cc b/pthread_test/bug1.cc
new file mode 100644 (file)
index 0000000..16d2b59
--- /dev/null
+++ b/pthread_test/bug1.cc
@@ -0,0 +1,74 @@
+/**
+ * @file iriw.cc
+ * @brief Independent read and independent write test
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+
+#define N 14
+//#include "wildcard.h"
+//#include "model-assert.h"
+
+using namespace std;
+
+std::atomic_int x, y;
+int r1, r2, r3, r4; /* "local" variables */
+
+static void *a(void *obj)
+{
+//     x.store(1, memory_order_seq_cst);
+       return NULL;
+}
+
+
+static void *b(void *obj)
+{
+       y.store(1, memory_order_seq_cst);
+       return NULL;
+}
+
+static void *c(void *obj)
+{
+       r1 = x.load(memory_order_acquire);
+       r2 = y.load(memory_order_seq_cst);
+       return NULL;
+}
+
+static void *d(void *obj)
+{
+       r3 = y.load(memory_order_acquire);
+       r4 = x.load(memory_order_seq_cst);
+       return NULL;
+}
+
+
+int user_main(int argc, char **argv)
+{
+       pthread_t threads[20];
+
+       atomic_init(&x, 0);
+       atomic_init(&y, 0);
+
+       printf("Main thread: creating %d threads\n", N);
+
+       for (int i = 0; i< N; i++)
+               pthread_create(&threads[i],NULL, &a, NULL);
+
+       for (int i=0; i<N; i++)
+               printf("thread id: %ld\n", threads[i]);
+
+       for (int i = 0; i< N; i++)
+               pthread_join( threads[i],NULL);
+
+       printf("Main thread is finished\n");
+
+       /*
+        * This condition should not be hit if the execution is SC */
+//     bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
+//     printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4);
+//     MODEL_ASSERT(!sc);
+
+       return 0;
+}

diff --git a/pthread_test/condvar.cc b/pthread_test/condvar.cc
new file mode 100644 (file)
index 0000000..aae622b
--- /dev/null
+++ b/pthread_test/condvar.cc
@@ -0,0 +1,44 @@
+#include <stdio.h>
+
+#include "pthread.h"
+#include "librace.h"
+#include "stdatomic.h"
+#include "mutex.h"
+#include <condition_variable>
+
+cdsc::mutex * m;
+cdsc::condition_variable *v;
+int shareddata;
+
+static void *a(void *obj)
+{
+       m->lock();
+       while(load_32(&shareddata)==0)
+               v->wait(*m);
+       m->unlock();
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       m->lock();
+       store_32(&shareddata, (unsigned int) 1);
+       v->notify_all();
+       m->unlock();
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2;
+       store_32(&shareddata, (unsigned int) 0);
+       m=new cdsc::mutex();
+       v=new cdsc::condition_variable();
+
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       return 0;
+}

diff --git a/pthread_test/deadlock.cc b/pthread_test/deadlock.cc
new file mode 100644 (file)
index 0000000..4382819
--- /dev/null
+++ b/pthread_test/deadlock.cc
@@ -0,0 +1,47 @@
+#include <stdio.h>
+#include <pthread.h>
+
+#include "librace.h"
+
+pthread_mutex_t x;
+pthread_mutex_t y;
+uint32_t shared = 0;
+
+static void *a(void *obj)
+{
+       pthread_mutex_lock(&x);
+       pthread_mutex_lock(&y);
+       printf("shared = %u\n", load_32(&shared));
+       pthread_mutex_unlock(&y);
+       pthread_mutex_unlock(&x);
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       pthread_mutex_lock(&y);
+       pthread_mutex_lock(&x);
+       store_32(&shared, 16);
+       printf("write shared = 16\n");
+       pthread_mutex_unlock(&x);
+       pthread_mutex_unlock(&y);
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2;
+
+       pthread_mutex_init(&x, NULL);
+       pthread_mutex_init(&y, NULL);
+
+       printf("Main thread: creating 2 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       printf("Main thread is finished\n");
+
+       return 0;
+}

diff --git a/pthread_test/insanesync.cc b/pthread_test/insanesync.cc
new file mode 100644 (file)
index 0000000..bcc34ad
--- /dev/null
+++ b/pthread_test/insanesync.cc
@@ -0,0 +1,72 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+#include <atomic>
+
+#include "librace.h"
+#include "model-assert.h"
+
+using namespace std;
+
+atomic_int x, y;
+atomic_intptr_t z, z2;
+
+int r1, r2, r3; /* "local" variables */
+
+/**
+               This example illustrates a self-satisfying cycle involving
+               synchronization.  A failed synchronization creates the store that
+               causes the synchronization to fail.
+
+               The C++11 memory model nominally allows r1=0, r2=1, r3=5.
+
+               This example is insane, we don't support that behavior.
+*/
+
+
+static void *a(void *obj)
+{
+       z.store((intptr_t)&y, memory_order_relaxed);
+       r1 = y.fetch_add(1, memory_order_release);
+       z.store((intptr_t)&x, memory_order_relaxed);
+       r2 = y.fetch_add(1, memory_order_release);
+       return NULL;
+}
+
+
+static void *b(void *obj)
+{
+       r3 = y.fetch_add(1, memory_order_acquire);
+       intptr_t ptr = z.load(memory_order_relaxed);
+       z2.store(ptr, memory_order_relaxed);
+       return NULL;
+}
+
+static void *c(void *obj)
+{
+       atomic_int *ptr2 = (atomic_int *)z2.load(memory_order_relaxed);
+       (*ptr2).store(5, memory_order_relaxed);
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2, t3;
+
+       atomic_init(&x, 0);
+       atomic_init(&y, 0);
+       atomic_init(&z, (intptr_t) &x);
+       atomic_init(&z2, (intptr_t) &x);
+
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+       pthread_create(&t3,NULL, &c, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       pthread_join(t3,NULL);
+
+       printf("r1=%d, r2=%d, r3=%d\n", r1, r2, r3);
+
+       return 0;
+}

diff --git a/pthread_test/iriw.cc b/pthread_test/iriw.cc
new file mode 100644 (file)
index 0000000..42ba936
--- /dev/null
+++ b/pthread_test/iriw.cc
@@ -0,0 +1,71 @@
+/**
+ * @file iriw.cc
+ * @brief Independent read and independent write test
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+
+#include "wildcard.h"
+#include "model-assert.h"
+
+using namespace std;
+
+atomic_int x, y;
+int r1, r2, r3, r4; /* "local" variables */
+
+static void *a(void *obj)
+{
+       x.store(1, memory_order_seq_cst);
+       return new int(1);
+}
+
+static void *b(void *obj)
+{
+       y.store(1, memory_order_seq_cst);
+       return new int(2);
+}
+
+static void *c(void *obj)
+{
+       r1 = x.load(memory_order_acquire);
+       r2 = y.load(memory_order_seq_cst);
+       return new int(3);
+}
+
+static void *d(void *obj)
+{
+       r3 = y.load(memory_order_acquire);
+       r4 = x.load(memory_order_seq_cst);
+       return new int(4);
+}
+
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2, t3, t4;
+
+       atomic_init(&x, 0);
+       atomic_init(&y, 0);
+
+       printf("Main thread: creating 4 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+       pthread_create(&t3,NULL, &c, NULL);
+       pthread_create(&t4,NULL, &d, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       pthread_join(t3,NULL);
+       pthread_join(t4,NULL);
+       printf("Main thread is finished\n");
+
+       /*
+        * This condition should not be hit if the execution is SC */
+       bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
+       printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4);
+       MODEL_ASSERT(!sc);
+
+       return 0;
+}

diff --git a/pthread_test/iriw_wildcard.cc b/pthread_test/iriw_wildcard.cc
new file mode 100644 (file)
index 0000000..adea420
--- /dev/null
+++ b/pthread_test/iriw_wildcard.cc
@@ -0,0 +1,70 @@
+/**
+ * @file iriw.cc
+ * @brief Independent read and independent write test
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+
+#include "wildcard.h"
+#include "model-assert.h"
+
+using namespace std;
+
+atomic_int x, y;
+int r1, r2, r3, r4; /* "local" variables */
+
+static void *a(void *obj)
+{
+       x.store(1, wildcard(1));
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       y.store(1, wildcard(2));
+       return NULL;
+}
+
+static void *c(void *obj)
+{
+       r1 = x.load(wildcard(3));
+       r2 = y.load(wildcard(4));
+       return NULL;
+}
+
+static void *d(void *obj)
+{
+       r3 = y.load(wildcard(5));
+       r4 = x.load(wildcard(6));
+       return NULL;
+}
+
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2, t3, t4;
+
+       atomic_init(&x, 0);
+       atomic_init(&y, 0);
+
+       printf("Main thread: creating 4 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+       pthread_create(&t3,NULL, &c, NULL);
+       pthread_create(&t4,NULL, &d, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       pthread_join(t3,NULL);
+       pthread_join(t4,NULL);
+       printf("Main thread is finished\n");
+
+       /*
+        * This condition should not be hit if the execution is SC */
+       bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
+       //MODEL_ASSERT(!sc);
+
+       return 0;
+}

diff --git a/pthread_test/mo-satcycle.cc b/pthread_test/mo-satcycle.cc
new file mode 100644 (file)
index 0000000..d0a6055
--- /dev/null
+++ b/pthread_test/mo-satcycle.cc
@@ -0,0 +1,71 @@
+/**
+ * @file mo-satcycle.cc
+ * @brief MO satisfaction cycle test
+ *
+ * This program has a peculiar behavior which is technically legal under the
+ * current C++ memory model but which is a result of a type of satisfaction
+ * cycle. We use this as justification for part of our modifications to the
+ * memory model when proving our model-checker's correctness.
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+
+#include "model-assert.h"
+
+using namespace std;
+
+atomic_int x, y;
+int r0, r1, r2, r3; /* "local" variables */
+
+static void *a(void *obj)
+{
+       y.store(10, memory_order_relaxed);
+       x.store(1, memory_order_release);
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       r0 = x.load(memory_order_relaxed);
+       r1 = x.load(memory_order_acquire);
+       y.store(11, memory_order_relaxed);
+       return NULL;
+}
+
+static void *c(void *obj)
+{
+       r2 = y.load(memory_order_relaxed);
+       r3 = y.load(memory_order_relaxed);
+       if (r2 == 11 && r3 == 10)
+               x.store(0, memory_order_relaxed);
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2, t3;
+
+       atomic_init(&x, 0);
+       atomic_init(&y, 0);
+
+       printf("Main thread: creating 3 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+       pthread_create(&t3,NULL, &c, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       pthread_join(t3,NULL);
+       printf("Main thread is finished\n");
+
+       /*
+        * This condition should not be hit because it only occurs under a
+        * satisfaction cycle
+        */
+       bool cycle = (r0 == 1 && r1 == 0 && r2 == 11 && r3 == 10);
+       MODEL_ASSERT(!cycle);
+
+       return 0;
+}

diff --git a/pthread_test/normal_compile.sh b/pthread_test/normal_compile.sh
new file mode 100755 (executable)
index 0000000..56cba5a
--- /dev/null
+++ b/pthread_test/normal_compile.sh
@@ -0,0 +1,9 @@
+#g++ -o test.o test.cc -Wall -g -O3 -I.. -I../include -L.. -lmodel
+
+export LD_LIBRARY_PATH=/scratch/random-fuzzer
+
+if [ "$2" != "" ]; then
+  g++ -o "$1.o" $1 -Wall -g -O3 -I.. -I../include -L.. -lmodel
+else
+  gcc -o "$1.o" $1 -Wall -g -O3 -I.. -I../include -L.. -lmodel
+fi

diff --git a/pthread_test/protect/mutex_test.cc b/pthread_test/protect/mutex_test.cc
new file mode 100644 (file)
index 0000000..9a84b1d
--- /dev/null
+++ b/pthread_test/protect/mutex_test.cc
@@ -0,0 +1,41 @@
+#include <stdio.h> 
+ 
+#include "threads.h" 
+#include "librace.h" 
+#include "stdatomic.h" 
+#include <pthread.h>
+
+int shareddata;  
+pthread_mutex_t m;
+
+static void* a(void *obj) 
+{ 
+        int i; 
+        for(i=0;i<2;i++) { 
+                if ((i%2)==0) { 
+                        pthread_mutex_lock(&m);
+                        store_32(&shareddata,(unsigned int)i); 
+                       printf("shareddata: %d\n", shareddata);
+                        pthread_mutex_unlock(&m);
+                } else { 
+                        while(!pthread_mutex_trylock(&m))
+                                thrd_yield(); 
+                        store_32(&shareddata,(unsigned int)i); 
+                       printf("shareddata: %d\n", shareddata);
+                        pthread_mutex_unlock(&m);
+                } 
+        } 
+} 
+ 
+int user_main(int argc, char **argv) 
+{ 
+        thrd_t t1, t2; 
+       pthread_mutex_init(&m, NULL);
+
+        thrd_create(&t1, (thrd_start_t)&a, NULL);
+        thrd_create(&t2, (thrd_start_t)&a, NULL);
+
+        thrd_join(t1); 
+        thrd_join(t2); 
+        return 0; 
+}

diff --git a/pthread_test/pthread_mutex_test.cc b/pthread_test/pthread_mutex_test.cc
new file mode 100644 (file)
index 0000000..55bea22
--- /dev/null
+++ b/pthread_test/pthread_mutex_test.cc
@@ -0,0 +1,69 @@
+#include <stdio.h>
+#include <pthread.h>
+#define NTHREADS 2
+void *thread_function(void *);
+//pthread_mutex_t mutex1; 
+
+int counter=0;
+
+class Box {
+public:
+//     int counter;
+
+       static Box& getInstance() {
+               static Box instance;
+               return instance;
+       }
+
+       void addone() {
+               pthread_mutex_lock(&pool_mutex);
+               counter++;
+               pthread_mutex_unlock(&pool_mutex);
+       }
+
+private:
+       Box() { 
+               pthread_mutex_init(&pool_mutex, NULL); 
+               counter = 0;
+       }
+       pthread_mutex_t pool_mutex;
+};
+
+int user_main(int argv, char **argc)
+{
+//   void *dummy = NULL;
+//   pthread_mutex_init(&mutex1, NULL); /* PTHREAD_MUTEX_INITIALIZER;*/
+
+//   pthread_t thread_id[NTHREADS];
+//   int i, j;
+
+   Box::getInstance().addone();
+
+/*   for(i=0; i < NTHREADS; i++)
+   {
+      pthread_create( &thread_id[i], NULL, &thread_function, NULL );
+   }
+
+   for(j=0; j < NTHREADS; j++)
+   {
+      pthread_join( thread_id[j], NULL); 
+   }
+*/
+ 
+   printf("Final counter value: %d\n", counter);
+   /*
+   for (i=0;i<NTHREADS; i++) {
+      printf("id %ld\n", thread_id[i]);
+   }*/
+   return 0;
+}
+
+void *thread_function(void *dummyPtr)
+{
+//   printf("Thread number %ld\n", pthread_self());
+   Box::getInstance().addone();
+//   pthread_mutex_lock( &mutex1 );
+//   Box::getInstance().counter++;
+//   pthread_mutex_unlock( &mutex1 );
+   return NULL;
+}

diff --git a/pthread_test/test.cc b/pthread_test/test.cc
new file mode 100644 (file)
index 0000000..f5b0857
--- /dev/null
+++ b/pthread_test/test.cc
@@ -0,0 +1,73 @@
+/**
+ * @file iriw.cc
+ * @brief Independent read and independent write test
+ */
+
+#include <atomic>
+#include <pthread.h>
+#include <stdio.h>
+#include <iostream>
+
+#define N 4
+//#include "wildcard.h"
+//#include "model-assert.h"
+
+using namespace std;
+
+atomic<int> x(1);
+atomic<int> y(1);
+
+int r1, r2, r3, r4; /* "local" variables */
+
+static void *a(void *obj)
+{
+       x.store(1, memory_order_relaxed);
+       y.store(1, memory_order_relaxed);
+
+       return new int(1);
+}
+
+
+static void *b(void *obj)
+{
+       y.store(1, memory_order_relaxed);
+       
+       return new int(2);
+}
+
+static void *c(void *obj)
+{
+       r1 = x.load(memory_order_acquire);
+       r2 = y.load(memory_order_relaxed);
+
+       return new int(3);
+}
+
+static void *d(void *obj)
+{
+       r3 = y.load(memory_order_acquire);
+       r4 = x.load(memory_order_relaxed);
+
+       return new int(4);
+}
+
+
+int main(int argc, char **argv)
+{
+       printf("Main thread starts\n");
+
+       x.store(2, memory_order_relaxed);
+       y.store(2, memory_order_relaxed);
+
+       r1 = x.load(memory_order_relaxed);
+       printf("%d\n", r1);
+
+//     x.compare_exchange_strong(r1, r2);
+//     r3 = x.load(memory_order_relaxed);
+
+//     printf("%d\n", r3);
+
+       printf("Main thread is finished\n");
+
+       return 0;
+}

diff --git a/pthread_test/uninit.cc b/pthread_test/uninit.cc
new file mode 100644 (file)
index 0000000..075e2ac
--- /dev/null
+++ b/pthread_test/uninit.cc
@@ -0,0 +1,57 @@
+/**
+ * @file uninit.cc
+ * @brief Uninitialized loads test
+ *
+ * This is a test of the "uninitialized loads" code. While we don't explicitly
+ * initialize y, this example's synchronization pattern should guarantee we
+ * never see it uninitialized.
+ */
+#include <stdio.h>
+#include <pthread.h>
+#include <atomic>
+
+//#include "librace.h"
+
+std::atomic_int x;
+std::atomic_int y;
+
+static void *a(void *obj)
+{
+       int flag = x.load(std::memory_order_acquire);
+       printf("flag: %d\n", flag);
+       if (flag == 2)
+               printf("Load: %d\n", y.load(std::memory_order_relaxed));
+       return NULL;
+}
+
+static void *b(void *obj)
+{
+       printf("fetch_add: %d\n", x.fetch_add(1, std::memory_order_relaxed));
+       return NULL;
+}
+
+static void *c(void *obj)
+{
+       y.store(3, std::memory_order_relaxed);
+       x.store(1, std::memory_order_release);
+       return NULL;
+}
+
+int user_main(int argc, char **argv)
+{
+       pthread_t t1, t2, t3;
+
+       std::atomic_init(&x, 0);
+
+       printf("Main thread: creating 3 threads\n");
+       pthread_create(&t1,NULL, &a, NULL);
+       pthread_create(&t2,NULL, &b, NULL);
+       pthread_create(&t3,NULL, &c, NULL);
+
+       pthread_join(t1,NULL);
+       pthread_join(t2,NULL);
+       pthread_join(t3,NULL);
+       printf("Main thread is finished\n");
+
+       return 0;
+}