Automatic Safety Proofs for Asynchronous Memory Operations
Asynchronous memory operations are an important feature of modern multicore systems. They provide a means for coping with the high cost of shared memory access: cores can delegate data movement to dedicated hardware, and continue processing on fast, private memory, without contention. Asynchronous memory operations are widely available, e.g. DMA operations in the cell BE, I/O acceleration technology in Intel Xeon cores, and asynchronous memory copying in CUDA/OpenCL. The high performance permitted by asynchronous memory operations comes at a price: increased programming complexity.