US 12,079,102 B2
Systems, methods, and media for proving the correctness of software on relaxed memory hardware
Ronghui Gu, New York, NY (US); Jason Nieh, New York, NY (US); and Runzhou Tao, New York, NY (US)
Assigned to The Trustees of Columbia University in the City of New York, New York, NY (US)
Filed by Ronghui Gu, New York, NY (US); Jason Nieh, New York, NY (US); and Runzhou Tao, New York, NY (US)
Filed on Jul. 14, 2021, as Appl. No. 17/376,120.
Claims priority of provisional application 63/190,674, filed on May 19, 2021.
Claims priority of provisional application 63/051,710, filed on Jul. 14, 2020.
Prior Publication US 2022/0019514 A1, Jan. 20, 2022
Int. Cl. G06F 11/36 (2006.01)
CPC G06F 11/3604 (2013.01) 18 Claims
OG exemplary drawing
 
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.