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.

Language Constructs and Features (acm D.3.3), Concurrent Programming (acm D.1.3), Language Classifications (acm D.3.2), Modes of Computation (acm F.1.2), Requirements/Specifications (acm D.2.1)
Programming languages (msc 68N15), Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10)
Software (theme 1), Software (theme 1)
Software Engineering [SEN]
Computer Security

Everaars, C.T.H, & Lisser, B. (1998). Coordination of a parallel proposition solver. Software Engineering [SEN]. CWI.