Yes, having access to multiple cores means that one can process some things faster. But performance is not the focus of this work, although that is a happy side

Yes, having access to multiple cores means that one can process some things faster. But performance is not the focus of this work, although that is a happy side effect. The focus is on correctness of concurrent code. CertiKOS's model explicitly accounts for the presence of concurrent processors accessing memory in an arbitrarily interleaved fashion. In order to get the verification process to sign off on a particular architecture, all accesses to shared memory _must_ use the correct synchronization primitives and memory barriers, among other things.