TY - GEN
T1 - Per-Location Simulation
AU - Li, Liyi
AU - Gunter, Elsa L.
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - Simulation/bisimulation is one of the most widely used frameworks for proving program equivalence/semantic preservation. In this paper, we propose a new per-location simulation (PLS) relation that is simple and suitable for proving that a compiled program semantically preserves its original program under a CFG-based language with a real-world, C/C++ like, weak memory model. To the best of our knowledge, PLS is the first simulation framework weaker than the CompCert[26]/CompCertTSO[47] one that is used for proving compiler correctness. With a combination of PLS, the compiler proof-framework Morpheus[34], and a language semantics with a weak memory model, we are able to prove that programs are semantically preserved through a transformation. All the definitions and proofs have been implemented in Isabelle/HOL.
AB - Simulation/bisimulation is one of the most widely used frameworks for proving program equivalence/semantic preservation. In this paper, we propose a new per-location simulation (PLS) relation that is simple and suitable for proving that a compiled program semantically preserves its original program under a CFG-based language with a real-world, C/C++ like, weak memory model. To the best of our knowledge, PLS is the first simulation framework weaker than the CompCert[26]/CompCertTSO[47] one that is used for proving compiler correctness. With a combination of PLS, the compiler proof-framework Morpheus[34], and a language semantics with a weak memory model, we are able to prove that programs are semantically preserved through a transformation. All the definitions and proofs have been implemented in Isabelle/HOL.
UR - http://www.scopus.com/inward/record.url?scp=85089719999&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089719999&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-55754-6_16
DO - 10.1007/978-3-030-55754-6_16
M3 - Conference contribution
AN - SCOPUS:85089719999
SN - 9783030557539
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 267
EP - 287
BT - NASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings
A2 - Lee, Ritchie
A2 - Jha, Susmit
A2 - Mavridou, Anastasia
PB - Springer
T2 - 12th International Symposium on NASA Formal Methods, NFM 2020
Y2 - 11 May 2020 through 15 May 2020
ER -