Synthesizing and Verifying Multicore Parallelism in Categories of Nested Code Graphs

Among the first generation of such processors, the Cell Broadband Engine (BE) is the most widely deployed. Using its resources efficiently requires explicit synchronisation of both code and data, and packaging of both to fit in small memory spaces and constrained communication infrastructures.