Verification of Cell Programs. The Cell Broadband Engine processor [72] is a heterogeneous multicore architecture (see Section 3.1.1) consisting of a host processor, the power processor element (PPE) and eight accelerator processors, the synergistic processor elements (SPEs). The system has segmented memory (see Section 3.2.5): each SPE has its own portion of scratch-pad memory which can be accessed without contention. A thread running on an SPE must explicitly copy data to/from main memory from/to its scratch-pad memory using direct memory access (DMA) operations. In order to hide latency, an SPE thread can launch many DMA operations simultaneously, and must ensure that concurrent DMA operations do not race: if two DMA operations are simultaneously pending, either issued by the same or different threads, and if these operations access overlapping regions of memory, then neither operation can modify this overlapping region of memory, otherwise undefined results will be computed. A static technique for detecting races between DMA operations issued by a single SPE thread has been proposed, based on bounded model checking [48, 49]. In this approach, DMA operations are tracked by instrumentation variables, and assertions are added to the program under analysis such that a failed assertion indicates a DMA race. This work also shows that the k-induction method [118, 46] can be used to prove absence of DMA races in programs that use multi-buffering as a latency hiding technique. This DMA race analysis technique is implemented in the SCRATCH tool [50], which builds on the bounded model checker CBMC [33]. Another technique for static verification of programs that use DMA operations, based on separation logic [20, 19], is discussed in Section 6.3.1.
