Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures

Robert J. Colvin, Ian J. Hayes, Scott Heiner +3

Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A partic…