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