We present the Multi-Core layer of the larger Coconut project to support high-performance,

high-assurance scientific computation. Programs are represented by nested code graphs, using

domain specific languages.


At the Multi-Core level, the language is very restricted, in order to restrict control flow to

non-branching, synchronising control flow, which allows us to treat multi-core parallelism

in essentially the same way as instruction-level parallelism for pipelined multi-issue processors.

The resulting schedule is then presented as a “locally sequential program", which, like high-quality

conventional assembly code in the single-core case, is arranged for hiding latencies at execution time

so that peak performance can be reached, and can also be understood by programmers. We present an

efficient, incremental algorithm capable of verifying the soundness of the communication aspects of

such programs.