Coordination of a parallel proposition solver

In this paper we describe an experiment in which {sc Manifold is used to coordinate the interprocess communication in a parallelized proposition solver. {sc Manifold is very well suited for applications involving dynamic process creation and dynamically changing (ir)regular communication patterns among sets of independent concurrent cooperating processes. The idea in this case study is simple. The proposition solver consists of a fixed numbers of separate processing units which communicate with each other such that the output of one serves as the input for the other. Because one of the processing units performs a computation intensive job, we introduce a master/worker protocol to divide its computations. We show that this protocol implemented in {sc Manifold adds another hierarchic layer to the application but leaves the previous layers intact. This modularity of {sc Manifold offers the possibility to introduce concurrency step by step. We also verify the implementation of the proposition solver using a simple family of assertions and give some performance results.