Verified Multicore Parallelism Using Atomic Verifiable Operations

Parallel computer architectures have now become almost universal, with even mobile phones containing dual core processors. Taking full advantage of the performance available in a computer system requires taking full advantage of the parallelism offered by that system. Opposed to the need for high performance is the need to verify the code’s requirements. Programming such architectures has long been recognized as a difficult task. Both requirements for performance and verifiability are difficult to attain.