Systems, methods, and media for proving the correctness of software on relaxed memory hardware
View Patent ↗Mechanisms for proving the correctness of software on relaxed memory hardware are provided, the mechanisms comprising: receiving a specification, a hardware model, and an implementation for the software to be executed on the relaxed memory hardware; evaluating the software using a sequentially consistent hardware model; evaluating the software using a relaxed memory hardware model and at least one of the following conditions: a data-race-free (DRF)-kernel condition; a no-barrier-misuse condition; a memory-isolation condition; a transactional-page-table condition; a write-once-kernel-mapping condition; and a weak-memory-isolation condition; and outputting an indication of whether the software is correct based on the evaluating the software using the sequentially consistent hardware model and the evaluating the software using the relaxed memory hardware model.
1. A method for proving the correctness of software on relaxed memory hardware, comprising:
receiving a specification, a hardware model, and an implementation for the software to be executed on the relaxed memory hardware;
executing a proof assistant on a collection of at least one hardware processor for evaluating the software using a sequentially consistent hardware model;
executing the proof assistant on the collection of at least one hardware processor for evaluating the software using a relaxed memory hardware model and a write-once-kernel-mapping condition in which entries of a shared page table of the software are only written to when the entries are empty; and
outputting an indication of whether the software is correct based on the evaluating the software using the sequentially consistent hardware model and the evaluating the software using the relaxed memory hardware model.
2. The method of claim 1 , wherein the evaluating the software using a relaxed memory hardware model further uses a data-race-free (DRF)-kernel condition.
3. The method of claim 2 , wherein the evaluating the software using a relaxed memory hardware model further uses a no-barrier-misuse condition.
4. The method of claim 3 , wherein the evaluating the software using a relaxed memory hardware model further uses a memory-isolation condition.
5. The method of claim 4 , wherein the evaluating the software using a relaxed memory hardware model further uses a transactional-page-table condition.
6. The method of claim 1 , wherein the evaluating the software using a relaxed memory hardware model further uses a weak-memory-isolation condition.
7. A system for proving the correctness of software on relaxed memory hardware, comprising:
a memory; and
a collection of at least one hardware processor coupled to the memory and configured to:
receive a specification, a hardware model, and an implementation for the software to be executed on the relaxed memory hardware;
execute a proof assistant for evaluating the software using a sequentially consistent hardware model;
execute the proof assistant for evaluating the software using a relaxed memory hardware model and a write-once-kernel-mapping condition in which entries of a shared page table of the software are only written to when the entries are empty; and
output an indication of whether the software is correct based on the evaluating the software using the sequentially consistent hardware model and the evaluating the software using the relaxed memory hardware model.
8. The system of claim 7 , wherein the evaluating the software using a relaxed memory hardware model further uses a data-race-free (DRF)-kernel condition.
9. The system of claim 8 , wherein the evaluating the software using a relaxed memory hardware model further uses a no-barrier-misuse condition.
10. The system of claim 9 , wherein the evaluating the software using a relaxed memory hardware model further uses a memory-isolation condition.
11. The system of claim 10 , wherein the evaluating the software using a relaxed memory hardware model further uses a transactional-page-table condition.
12. The system of claim 10 , wherein the evaluating the software using a relaxed memory hardware model further uses a weak-memory-isolation condition.
13. A non-transitory computer-readable medium containing computer executable instructions that, when executed by a first collection of at least one hardware processor, cause the first collection of at least one processor to perform a method for proving the correctness of software on relaxed memory hardware, the method comprising:
receiving a specification, a hardware model, and an implementation for the software to be executed on the relaxed memory hardware;
executing a proof assistant for evaluating the software using a sequentially consistent hardware model;
executing the proof assistant for evaluating the software using a relaxed memory hardware model and a write-once-kernel-mapping condition in which entries of a shared page table of the software are only written to when the entries are empty; and
outputting an indication of whether the software is correct based on the evaluating the software using the sequentially consistent hardware model and the evaluating the software using the relaxed memory hardware model.
14. The non-transitory computer-readable medium of claim 13 , wherein the evaluating the software using a relaxed memory hardware model further uses a data-race-free (DRF)-kernel condition.
15. The non-transitory computer-readable medium of claim 14 , wherein the evaluating the software using a relaxed memory hardware model further uses a no-barrier-misuse condition.
16. The non-transitory computer-readable medium of claim 15 , wherein the evaluating the software using a relaxed memory hardware model further uses a memory-isolation condition.
17. The non-transitory computer-readable medium of claim 16 , wherein the evaluating the software using a relaxed memory hardware model further uses a transactional-page-table condition.
18. The non-transitory computer-readable medium of claim 17 , wherein the evaluating the software using a relaxed memory hardware model further uses a weak-memory-isolation condition.