Merge branch 'ta/brick-update' into ta/bitstate

Update bricks library to latest 4.4.2 version.

spot/Makefile.am

@@ -22,8 +22,16 @@
 
 AUTOMAKE_OPTIONS = subdir-objects
 
-nobase_include_HEADERS= bricks/brick-assert bricks/brick-bitlevel \
-	bricks/brick-hash bricks/brick-hashset  bricks/brick-shmem \
+nobase_include_HEADERS= \
+	bricks/brick-assert \
+	bricks/brick-bitlevel \
+	bricks/brick-hash \
+	bricks/brick-hashset \
+	bricks/brick-min \
+	bricks/brick-ptr \
+	bricks/brick-shmem \
+	bricks/brick-string \
+	bricks/brick-trace \
 	bricks/brick-types
 
 

spot/bricks/brick-ptr

+// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
+
+/*
+ * (c) 2019 Petr Ročkai <code@fixp.eu>
+ *
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#pragma once
+
+// FIX HERE: use #include "" instead of #include <>
+#include "brick-assert"
+#include <atomic>
+
+namespace brq
+{
+    template< typename T, bool atomic = false >
+    struct refcount_ptr
+    {
+        refcount_ptr() noexcept = default;
+        refcount_ptr( const refcount_ptr< T, atomic > &o ) noexcept : refcount_ptr( o._ptr ) {}
+        refcount_ptr( T *v ) noexcept : _ptr( v ) { _get(); }
+        template< typename D, typename = std::enable_if_t< std::is_convertible_v< D *, T * > > >
+        refcount_ptr( const refcount_ptr< D > &o ) noexcept : refcount_ptr( o._ptr ) {}
+        ~refcount_ptr() noexcept { _put(); }
+        T *operator->() const noexcept { return _ptr; }
+        T &operator*() const noexcept { return *_ptr; }
+
+        explicit operator bool() const noexcept { return ptr(); }
+        bool operator !() const noexcept { return !ptr(); }
+
+        bool operator==( const refcount_ptr &o ) const noexcept
+        {
+            return !( *this < o ) && !( o < *this );
+        }
+
+        bool operator!=( const refcount_ptr &o ) const noexcept
+        {
+            return *this < o || o < *this;
+        }
+
+        bool operator<( const refcount_ptr &o ) const noexcept
+        {
+            return std::less< const void * >()( ptr(), o.ptr() );
+        }
+
+        template< bool o_atomic >
+        refcount_ptr< T, atomic > &operator=( const refcount_ptr< T, o_atomic > &o ) noexcept
+        {
+            if constexpr ( o_atomic == atomic ) /* atomic and !atomic can't alias each other */
+                if ( &o == this )
+                    return *this;
+
+            _put();
+            ptr( o.ptr() );
+            _get();
+            return *this;
+        }
+
+        refcount_ptr< T, atomic > &operator=( const refcount_ptr< T, atomic > &o ) noexcept
+        {
+            return operator=< atomic >( o );
+        }
+
+        T *ptr() const noexcept
+        {
+            if constexpr ( atomic )
+            {
+                auto val = uintptr_t( _ptr.load() );
+                return reinterpret_cast< T * >( val & ~uintptr_t( 1 ) );
+            }
+            else
+                return _ptr;
+        }
+
+        void ptr( T *p ) const noexcept { if constexpr ( atomic ) _ptr.store( p ); else _ptr = p; }
+
+        void _get() const noexcept
+        {
+            auto p = ptr();
+            if ( p )
+                p->ref_get();
+        }
+
+        void _put() const noexcept
+        {
+            auto p = ptr();
+            if ( p && !p->ref_put() )
+                delete p, ptr( nullptr );
+        }
+
+        void reset( T *p = nullptr ) noexcept
+        {
+            if ( p )
+                p->ref_get();
+            _put();
+            ptr( p );
+        }
+
+        bool compare_exchange_strong( refcount_ptr< T, false > &p, refcount_ptr< T, false > n )
+        {
+            TRACE( "cmpxchg ", ptr(), p.ptr(), n.ptr() );
+            std::atomic< uintptr_t > &self = *reinterpret_cast< std::atomic< uintptr_t > * >( &_ptr );
+            uintptr_t expect = self.load() & ~uintptr_t( 1 );
+            uintptr_t want = expect | 1;
+
+            while ( !self.compare_exchange_weak( expect, want ) )
+                want = expect | 1, expect = expect & ~uintptr_t( 1 );
+
+            uintptr_t self_val = want & ~uintptr_t( 1 );
+            T *self_ptr = reinterpret_cast< T * >( self_val );
+
+            if ( p.ptr() == self_ptr ) /* success, update this */
+            {
+                n._get();
+                p._put();
+                _ptr.store( n.ptr() );
+                return true;
+            }
+            else /* failed, update p */
+            {
+                if ( self_ptr )
+                    self_ptr->ref_get();
+                p._put();
+                p.ptr( self_ptr );
+                _ptr.store( self_ptr );
+                return false;
+            }
+        }
+
+        template< typename stream >
+        friend auto operator<<( stream &o, const refcount_ptr< T, atomic > &p )
+            -> decltype( o << std::declval< void * >() )
+        {
+            return o << p.ptr();
+        }
+
+        mutable std::conditional_t< atomic, std::atomic< T * >, T * > _ptr = nullptr;
+    };
+
+    template< typename T = uint16_t, bool atomic = false >
+    struct refcount_base
+    {
+        static constexpr const T max = std::numeric_limits< T >::max();
+
+        void ref_get()
+        {
+            if ( _refcount < max )
+                ++ _refcount;
+        }
+
+        bool ref_put()
+        {
+            ASSERT_LEQ( 1, _refcount );
+            return _refcount < max && --_refcount;
+        }
+
+        ~refcount_base() { NOISE( this, "destroyed" ); }
+        refcount_base() = default;
+        refcount_base( const refcount_base & ) : _refcount( 0 ) {}
+        refcount_base( refcount_base && ) : _refcount( 0 ) {}
+        refcount_base &operator=( refcount_base ) { return *this; }
+
+        std::conditional_t< atomic, std::atomic< T >, T > _refcount = 0;
+    };
+
+    template< typename T, typename... Args >
+    refcount_ptr< T > make_refcount( Args && ... args )
+    {
+        return refcount_ptr< T >( new T( std::forward< Args >( args )... ) );
+    }
+
+    template< typename T, bool atomic, typename... Args >
+    refcount_ptr< T, atomic > make_refcount_opt( Args && ... args )
+    {
+        return refcount_ptr< T, atomic >( new T( std::forward< Args >( args )... ) );
+    }
+}
+
+namespace t_brq
+{
+    template< bool atomic >
+    struct ref_test : brq::refcount_base< uint16_t, atomic >
+    {
+        int &cnt;
+        ref_test( int &cnt ) : cnt( cnt ) { ++cnt; }
+        ~ref_test() { --cnt; }
+    };
+
+    template< bool atomic_ptr, bool atomic_cnt >
+    struct refcount_ptr
+    {
+        struct obj : brq::refcount_base< uint16_t, atomic_cnt > {};
+
+        TEST(simple)
+        {
+            auto a = brq::make_refcount_opt< obj, atomic_ptr >();
+            ASSERT_EQ( a->_refcount, 1 );
+        }
+
+        TEST(dtor)
+        {
+            auto a = brq::make_refcount_opt< obj, atomic_ptr >();
+            ASSERT_EQ( a->_refcount, 1 );
+            {
+                auto b = a;
+                ASSERT_EQ( a->_refcount, 2 );
+            }
+            ASSERT_EQ( a->_refcount, 1 );
+        }
+
+        TEST(assign)
+        {
+            auto a = brq::make_refcount_opt< obj, atomic_ptr >();
+            decltype( a ) b;
+            ASSERT_EQ( a->_refcount, 1 );
+            b = a;
+            ASSERT_EQ( a->_refcount, 2 );
+            *&b = b;
+            ASSERT_EQ( a->_refcount, 2 );
+        }
+
+        TEST(destroy)
+        {
+            int objs = 0;
+            {
+                auto a = brq::make_refcount_opt< ref_test< atomic_cnt >, atomic_ptr >( objs );
+                ASSERT_EQ( objs, 1 );
+            }
+            ASSERT_EQ( objs, 0 );
+        }
+    };
+
+    template struct refcount_ptr< true, true >;
+    template struct refcount_ptr< false, true >;
+    template struct refcount_ptr< true, false >;
+    template struct refcount_ptr< false, false >;
+}
+
+// vim: syntax=cpp tabstop=4 shiftwidth=4 expandtab

spot/bricks/brick-shmem

@@ -37,6 +37,9 @@
  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  * POSSIBILITY OF SUCH DAMAGE. */
 
+#pragma once
+
+// FIX HERE: use #include "" instead of #include <>
 #include "brick-assert"
 #include <deque>
 #include <iostream>
@@ -50,9 +53,6 @@
 #include <unistd.h> // alarm
 #include <vector>
 
-#ifndef BRICK_SHMEM_H
-#define BRICK_SHMEM_H
-
 #ifndef BRICKS_CACHELINE
 #define BRICKS_CACHELINE 64
 #endif
@@ -71,11 +71,10 @@ template< typename T >
 struct Thread : T, ThreadBase
 {
     std::unique_ptr< std::thread > _thread;
-    bool _start_on_move = false; // :-(
+    bool _start_on_move; // :-(
 
     template< typename... Args >
-    Thread( Args&&... args ) : T( std::forward< Args >( args )... )
-    {}
+    Thread( Args&&... args ) : T( std::forward< Args >( args )... ), _start_on_move( false ) {}
     virtual ~Thread() { stop(); }
 
     Thread( const Thread &other ) : T( other )
@@ -85,21 +84,22 @@ struct Thread : T, ThreadBase
     }
 
     Thread( Thread &&other )
-        : T(other)
+        : T( other._thread ? throw std::logic_error( "cannot move a running thread" ) : other ),
+          _thread( std::move( other._thread ) ),
+          _start_on_move( false )
     {
-        if (other._thread)
-            throw std::logic_error( "cannot move a running thread" );
-        
-        _thread =  std::move( other._thread );
         if ( other._start_on_move )
             start();
     }
 
+    // FIX HERE: add override
     virtual void start() override
     {
+        // FIX HERE: add noexcept
         _thread.reset( new std::thread( [this]() noexcept { this->main(); } ) );
     }
 
+    // FIX HERE: add override
     virtual void stop() override
     {
         if ( _thread && _thread->joinable() )
@@ -177,13 +177,13 @@ struct AsyncLoop : Thread< LoopWrapper< T > >
         stop(); /* call the correct stop(), with interrupt() */
     }
 
-    void start() override
+    void start()
     {
         this->_interrupted.store( false, std::memory_order_relaxed );
         Super::start();
     }
 
-    void stop() override
+    void stop()
     {
         this->interrupt();
         Super::stop();
@@ -198,7 +198,7 @@ auto async_loop( L &&l )
 {
     AsyncLambdaLoop< L > al( std::forward< L >( l ) );
     al._start_on_move = true;
-    return al;
+    return std::move( al );
 }
 
 template< typename L >
@@ -206,7 +206,7 @@ auto thread( L &&l )
 {
     Thread< LambdaWrapper< L > > thr( std::forward< L >( l ) );
     thr._start_on_move = true;
-    return thr;
+    return std::move( thr );
 }
 
 template< typename T >
@@ -415,6 +415,117 @@ constexpr int defaultNodeSize() { return 3; }
  * to give good cache usage.
  */
 
+template< typename T, int NodeSize = defaultNodeSize< T >() >
+struct Fifo {
+protected:
+    // the Node layout puts read and write counters far apart to avoid
+    // them sharing a cache line, since they are always written from
+    // different threads
+    struct Node {
+        T *read               __attribute__((__aligned__(BRICKS_CACHELINE)));
+        T buffer[ NodeSize ]  __attribute__((__aligned__(BRICKS_CACHELINE)));
+        T * volatile write;
+        Node *next;
+        Node() {
+            read = write = buffer;
+            next = 0;
+        }
+    };
+
+    // pad the fifo object to ensure that head/tail pointers never
+    // share a cache line with anyone else
+    Node *head            __attribute__((__aligned__(BRICKS_CACHELINE)));
+    Node * volatile tail  __attribute__((__aligned__(BRICKS_CACHELINE)));
+
+public:
+    Fifo() {
+        head = tail = new Node();
+        ASSERT( empty() );
+    }
+
+    // copying a fifo is not allowed
+    Fifo( const Fifo & ) {
+        head = tail = new Node();
+        ASSERT( empty() );
+    }
+
+    ~Fifo() {
+        while ( head != tail ) {
+            Node *next = head->next;
+            ASSERT( next != 0 );
+            delete head;
+            head = next;
+        }
+        delete head;
+    }
+
+    void push( const T&x ) {
+        Node *t;
+        if ( tail->write == tail->buffer + NodeSize )
+            t = new Node();
+        else
+            t = tail;
+
+        *t->write = x;
+        ++ t->write;
+        __sync_synchronize();
+
+        if ( tail != t ) {
+            tail->next = t;
+            __sync_synchronize();
+            tail = t;
+        }
+    }
+
+    bool empty() {
+        return head == tail && head->read >= head->write;
+    }
+
+    int size() {
+    	int size = 0;
+    	Node *n = head;
+    	do {
+            size += n->write - n->read;
+            n = n->next;
+        } while (n);
+        return size;
+    }
+
+    void dropHead() {
+        Node *old = head;
+        head = head->next;
+        ASSERT( head );
+        delete old;
+    }
+
+    void pop() {
+        ASSERT( !empty() );
+        ++ head->read;
+        if ( head->read == head->buffer + NodeSize ) {
+            if ( head != tail ) {
+                dropHead();
+            }
+        }
+        // the following can happen when head->next is 0 even though head->read
+        // has reached NodeSize, *and* no front() has been called in the meantime
+        if ( head != tail && head->read > head->buffer + NodeSize ) {
+            dropHead();
+            pop();
+        }
+    }
+
+    T &front( bool wait = false ) {
+        while ( wait && empty() ) ;
+        ASSERT( head );
+        ASSERT( !empty() );
+        // last pop could have left us with empty queue exactly at an
+        // edge of a block, which leaves head->read == NodeSize
+        if ( head->read == head->buffer + NodeSize ) {
+            dropHead();
+        }
+        return *head->read;
+    }
+};
 
 /*
  * A very simple spinlock-protected queue based on std::deque.
@@ -534,9 +645,13 @@ namespace
 
 using steady_time = std::chrono::time_point< std::chrono::steady_clock >;
 
+steady_time later( int ms )
+{
+    return std::chrono::steady_clock::now() + std::chrono::milliseconds( ms );
+}
+
 template< typename I, typename F >
-std::future_status wait( I b, I e, F cleanup,
-                         steady_time until /*= 0 later( 500 )*/ ) try
+std::future_status wait( I b, I e, F cleanup, steady_time until = later( 500 ) ) try
 {
     int total = 0, ready = 0;
     for ( auto i = b; i != e; ++i )
@@ -555,6 +670,7 @@ std::future_status wait( I b, I e, F cleanup,
         return std::future_status::ready;
     }
     return std::future_status::timeout;
+// FIX HERE: remove extra ';' (-pedantic)
 } catch ( ... ) { cleanup(); throw; }
 
 }
@@ -574,8 +690,6 @@ static constexpr int size = 128 * 1024;
 
 #if defined( __unix ) || defined( POSIX )
 static void timeout() { alarm( 5 ); }
-#else
-static void timeout() {  }
 #endif
 
 struct ThreadTest
@@ -599,8 +713,58 @@ struct ThreadTest
     }
 };
 
+struct FifoTest {
+    template< typename T >
+    struct Checker
+    {
+        Fifo< T > fifo;
+        int terminate;
+        int n;
+
+        void main()
+        {
+            std::vector< int > x;
+            x.resize( n );
+            for ( int i = 0; i < n; ++i )
+                x[ i ] = 0;
+
+            while (true) {
+                while ( !fifo.empty() ) {
+                    int i = fifo.front();
+                    ASSERT_EQ( x[i % n], i / n );
+                    ++ x[ i % n ];
+                    fifo.pop();
+                }
+                if ( terminate > 1 )
+                    break;
+                if ( terminate )
+                    ++terminate;
+            }
+            terminate = 0;
+            for ( int i = 0; i < n; ++i )
+                ASSERT_EQ( x[ i ], size );
+        }
+
+        Checker( int _n = 1 ) : terminate( 0 ), n( _n ) {}
+    };
+
+    TEST(stress) {
+        Thread< Checker< int > > c;
+        for ( int j = 0; j < 5; ++j ) {
+            c.start();
+            for( int i = 0; i < size; ++i )
+                c.fifo.push( i );
+            c.terminate = true;
+            c.join();
+        }
+    }
+};
 
+#ifdef __divine__
+namespace { const int peers = 3; }
+#else
 namespace { const int peers = 12; }
+#endif
 
 struct Utils {
 
@@ -844,7 +1008,7 @@ struct Linked {
 
     Linked() {
         reader = writer = new Node();
-        reader->next = nullptr;
+        reader->next = 0;
     }
 };
 
@@ -1069,7 +1233,7 @@ struct FIFO : BenchmarkGroup
             case 1: return length_< LockedQueue< T > >();
             case 2: return length_< Linked< T > >();
             case 3: return length_< Ring< T  > >();
-                //            case 4: return length_< Fifo< T > >();
+            case 4: return length_< Fifo< T > >();
             case 5: return length_< Student< T > >();
             default: ASSERT_UNREACHABLE_F( "bad q = %d", q );
         }
@@ -1085,7 +1249,6 @@ struct FIFO : BenchmarkGroup
 }
 }
 
-#endif
 #endif
 
 // vim: syntax=cpp tabstop=4 shiftwidth=4 expandtab

spot/bricks/brick-trace

+// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
+
+/*
+ * Macros for run-time-configurable debug tracing.
+ */
+
+/*
+ * (c) 2019 Petr Ročkai <code@fixp.eu>
+ *
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#pragma once
+
+#include "brick-min"
+#include <array>
+
+#ifdef __divine__
+#include <sys/cdefs.h>
+#include <sys/trace.h>
+#include <util/array.hpp>
+#else
+#include <vector>
+#include <cstring>
+#include <pthread.h>
+#define __debugfn
+#define __boring
+#endif
+
+#ifdef __unix__
+#include <unistd.h>
+#include <syslog.h>
+#else
+#include <cstdio>
+#endif
+
+/* The purpose of the TRACE macro is to allow tracing statements to be included
+ * in production code, just like ASSERT macros allow for sanity checks and
+ * pre/post-condition checking. If compiled with NDEBUG, it's a noop and in
+ * debug builds, the output must be enabled by setting environment variables
+ * BRICK_TRACE and optionally BRICK_NOTRACE, which accept either `all`, a file
+ * name (without path) or a file name and a line number (formatted like
+ * `file.cpp:15`). A runtime-disabled trace point compiles to a few lookups in
+ * std::unordered_set.
+ *
+ * Normally, the formatted trace output is printed using std::cerr. The
+ * formatting is done using a brq::string_builder (see below) to cut down on
+ * overhead and to prevent exceptions being thrown. When built for DiOS, the
+ * output is done unconditionally using the __dios_trace mechanism, and the
+ * entire trace function is marked as __debugfn (i.e. it is not executed during
+ * model checking, only for counter-example generation -- TRACE therefore only
+ * causes very modest overhead in DIVINE). */
+
+#define BRICK_LOCATION(stmt) ::brq::trace_location{ __LINE__, __FILE__, stmt }
+
+#ifdef NDEBUG
+#define TRACE(...) static_cast< decltype(__VA_ARGS__, void(0)) >(0)
+#define NOISE(...) static_cast< decltype(__VA_ARGS__, void(0)) >(0)
+#else
+#define TRACE(...) ::brq::trace_fn< true >( 3, BRICK_LOCATION( "" ), __VA_ARGS__ )
+#define NOISE(...) ::brq::trace_fn< true >( 4, BRICK_LOCATION( "" ), __VA_ARGS__ )
+#endif
+// FIX HERE: DEBUG already defined in spot
+//#define DEBUG(...) ::brq::trace_fn< false >( 2, BRICK_LOCATION( "" ), __VA_ARGS__ )
+#define INFO(...)  ::brq::trace_fn< false >( 1, BRICK_LOCATION( "" ), __VA_ARGS__ )
+#define ERROR(...) ::brq::trace_fn< false >( 0, BRICK_LOCATION( "" ), __VA_ARGS__ )
+
+namespace brq
+{
+    /* Wrap __FILE__ and __LINE__, optionally together with a stringified
+     * assertion statement. Needs to be cheap to construct and pass around,
+     * since in debug builds this happens a lot. */
+