From 4c7305058b18e8ea8ab794d9d571a54e9ee0ea80 Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Tue, 25 Jun 2019 10:22:13 +0000
Subject: [PATCH] MC: Make task_queue (and hence the weaver) more flexible.
---
divine/mc/search.hpp | 50 ++++++++++++------------
divine/mc/t-search.hpp | 17 +++++----
divine/mc/t-weaver.hpp | 51 ++++++++++++-------------
divine/mc/weaver.hpp | 87 ++++++++++++++++++------------------------
4 files changed, 96 insertions(+), 109 deletions(-)
diff --git a/divine/mc/search.hpp b/divine/mc/search.hpp
index 44d51d660..bbdf52a56 100644
--- a/divine/mc/search.hpp
+++ b/divine/mc/search.hpp
@@ -19,41 +19,40 @@
#pragma once
#include <divine/mc/weaver.hpp>
-namespace divine::mc
+namespace divine::mc::task
{
template< typename State, typename Label >
- struct GraphTasks
+ struct Edge
{
- struct Edge
- {
- State from, to;
- Label label;
- bool isnew;
- Edge( State f, State t, Label l, bool n )
- : from( f ), to( t ), label( l ), isnew( n )
- {}
- };
-
- struct Expand
- {
- State from;
- Expand( State s ) : from( s ) {}
- };
+ State from, to;
+ Label label;
+ bool isnew;
+ Edge( State f, State t, Label l, bool n )
+ : from( f ), to( t ), label( l ), isnew( n )
+ {}
+ };
- struct Start {};
- using TQ_ = TaskQueue< GraphTasks< State, Label >, Start, Expand, Edge >;
+ template< typename State >
+ struct Expand
+ {
+ State from;
+ Expand( State s ) : from( s ) {}
};
+}
+namespace divine::mc
+{
template< typename State, typename Label >
- using GraphTQ = typename GraphTasks< State, Label >::TQ_;
+ using GraphTQ = task_queue< task::Start, task::Expand< State >, task::Edge< State, Label > >;
- template< typename TQ >
- struct Search : TQ::Skel
+ template< typename State, typename Label >
+ struct Search : GraphTQ< State, Label >::skeleton
{
- using Edge = typename TQ::Tasks::Edge;
- using Expand = typename TQ::Tasks::Expand;
+ using TQ = GraphTQ< State, Label >;
+ using Edge = task::Edge< State, Label >;
+ using Expand = task::Expand< State >;
- using TQ::Skel::run;
+ using TQ::skeleton::run;
void run( TQ &tq, Edge e )
{
@@ -61,5 +60,4 @@ namespace divine::mc
tq.template add< Expand >( e.to );
}
};
-
}
diff --git a/divine/mc/t-search.hpp b/divine/mc/t-search.hpp
index b601cb366..d97865f51 100644
--- a/divine/mc/t-search.hpp
+++ b/divine/mc/t-search.hpp
@@ -26,15 +26,19 @@
namespace divine::t_mc
{
enum Label { Red, Black };
- using TQ = mc::GraphTQ< int, Label >;
- struct Base : TQ::Skel
+ using TQ = mc::GraphTQ< int, Label >;
+ using Edge = mc::task::Edge< int, Label >;
+ using Expand = mc::task::Expand< int >;
+
+
+ struct Base : TQ::skeleton
{
brq::concurrent_hash_set< int > _states;
- using TQ::Skel::run;
+ using TQ::skeleton::run;
- void run( TQ &tq, typename TQ::Tasks::Start )
+ void run( TQ &tq, mc::task::Start )
{
_states.insert( 1 );
tq.add< Expand >( 1 );
@@ -126,13 +130,10 @@ namespace divine::t_mc
struct Search
{
- using Edge = TQ::Tasks::Edge;
- using Expand = TQ::Tasks::Expand;
-
template< typename B >
auto weave( B builder )
{
- return mc::Weaver< TQ >().extend( mc::Search< TQ >(), builder );
+ return mc::Weaver< TQ >().extend( mc::Search< int, Label >(), builder );
}
TEST( fixed )
diff --git a/divine/mc/t-weaver.hpp b/divine/mc/t-weaver.hpp
index 16dc53d58..aaa5f784a 100644
--- a/divine/mc/t-weaver.hpp
+++ b/divine/mc/t-weaver.hpp
@@ -22,57 +22,56 @@
namespace divine::t_mc
{
- struct Tasks
+ struct task1
{
- struct T1
- {
- int i;
- T1( int i ) : i( i ) {}
- };
+ int i;
+ task1( int i ) : i( i ) {}
+ };
- struct T2
- {
- int j;
- T2( int j ) : j( j ) {}
- };
+ struct task2
+ {
+ int j;
+ task2( int j ) : j( j ) {}
};
- using TQ = mc::TaskQueue< Tasks, Tasks::T1, Tasks::T2 >;
+ using tq = mc::task_queue< task1, task2 >;
- struct Machine1 : TQ::Skel
+ struct machine1 : tq::skeleton
{
- using TQ::Skel::run;
- void run( TQ &tq, Tasks::T1 t )
+ using tq::skeleton::run;
+
+ void run( tq &q, task1 t )
{
if ( t.i < 10 )
- tq.add< T2 >( t.i + 1 );
+ q.add< task2 >( t.i + 1 );
}
};
- struct Machine2 : TQ::Skel
+ struct machine2 : tq::skeleton
{
- using TQ::Skel::run;
- void run( TQ &tq, T2 t )
+ using tq::skeleton::run;
+
+ void run( tq &q, task2 t )
{
- tq.add< T1 >( t.j + 1 );
+ q.add< task1 >( t.j + 1 );
}
};
- struct Counter : Tasks
+ struct counter
{
int t1 = 0, t2 = 0;
- void run( TQ &, T1 ) { ++t1; }
- void run( TQ &, T2 ) { ++t2; }
+ void run( tq &, task1 ) { ++t1; }
+ void run( tq &, task2 ) { ++t2; }
};
struct Weave
{
TEST( basic )
{
- mc::Weaver< TQ, Machine1, Machine2, Counter > weaver;
- weaver.add< Tasks::T1 >( 3 );
+ mc::Weaver< tq, machine1, machine2, counter > weaver;
+ weaver.add< task1 >( 3 );
weaver.run();
- auto &ctr = weaver.machine< Counter >();
+ auto &ctr = weaver.machine< counter >();
ASSERT_EQ( ctr.t1, 5 );
ASSERT_EQ( ctr.t2, 4 );
}
diff --git a/divine/mc/weaver.hpp b/divine/mc/weaver.hpp
index 3bd43d804..bfb3f136c 100644
--- a/divine/mc/weaver.hpp
+++ b/divine/mc/weaver.hpp
@@ -19,76 +19,65 @@
#pragma once
#include <deque>
-namespace divine::mc
+namespace divine::mc::task
{
+ struct Start {};
+}
- template< typename... > struct MachineSkel;
-
- template< typename TS, typename TQ, typename Task, typename... Tasks >
- struct MachineSkel< TS, TQ, Task, Tasks... > : MachineSkel< TS, TQ, Tasks... >
- {
- using MachineSkel< TS, TQ, Tasks... >::run;
- void run( TQ &, Task ) {}
- };
+namespace divine::mc
+{
+ template< typename... > struct task_queue;
- template< typename TS, typename TQ >
- struct MachineSkel< TS, TQ > : TS
+ template<>
+ struct task_queue<>
{
- void run();
+ void clear();
+ template< typename P > bool process_next( P ) { return false; }
};
- template< typename TaskStruct, typename... TaskList >
- struct TaskQueue
+ template< typename task, typename... tasks >
+ struct task_queue< task, tasks... > : task_queue< tasks... >
{
- using TQ = TaskQueue< TaskStruct, TaskList... >;
- using Tasks = TaskStruct;
-
- template< typename TS >
- struct ExtendTS : TaskStruct, TS {};
+ using next = task_queue< tasks... >;
+ using tq = task_queue< task, tasks... >;
+ std::deque< task > _queue;
- template< typename TS, typename... Extra >
- using Extend = TaskQueue< ExtendTS< TS >, Extra..., TaskList... >;
+ template< typename... ex >
+ using extend = task_queue< ex..., tasks... >;
- using Queues = std::tuple< std::deque< TaskList > ... >;
- Queues _queues;
-
- template< typename Task, typename... Args >
+ template< typename T, typename... Args >
void add( Args... args )
{
- std::get< std::deque< Task > >( _queues ).emplace_back( args... );
+ if constexpr ( std::is_convertible_v< T, task > )
+ _queue.emplace_back( args... );
+ else
+ next::template add< T >( args... );
}
- template< int i = 0 >
void clear()
{
- if constexpr ( i < std::tuple_size_v< Queues > )
- {
- std::get< i >( _queues ).clear();
- return clear< i + 1 >();
- }
+ _queue.clear();
+ next::clear();
}
- template< int i = 0, typename P >
+ template< typename P >
bool process_next( P process )
{
- if constexpr ( i < std::tuple_size_v< Queues > )
+ if ( _queue.empty() )
+ return next::process_next( process );
+ else
{
- auto &q = std::get< i >( _queues );
-
- if ( !q.empty() )
- {
- process( q.front() );
- q.pop_front();
- return true;
- }
-
- return process_next< i + 1 >( process );
+ process( _queue.front() );
+ _queue.pop_front();
+ return true;
}
- else
- return false;
}
- using Skel = MachineSkel< TaskStruct, TQ, TaskList... >;
+ struct skeleton
+ {
+ template< typename T >
+ void run( tq &, const T & ) {}
+ };
};
template< typename TQ, typename... Machines >
@@ -213,12 +202,12 @@ namespace divine::mc
void run() /* TODO parallel */
{
auto process = [&]( auto t ) { process_task< 0 >( t ); };
- while ( _queue.template process_next< 0 >( process ) );
+ while ( _queue.process_next( process ) );
}
void start()
{
- add< typename TQ::Tasks::Start >();
+ add< task::Start >();
run();
}
};
--
GitLab