Comparison of an operational and an axiomatic model of execution for 
multi-threaded programs - presentation of the current status 


Relaxed memory consistency models, in contrast to the intuitive 
sequential consistency model, allow the use of modern hardware and 
compiler optimizations. Thereby they have a nontrivial influence on 
information flow security with respect to noninterference properties.
To clarify this influence, a generic operational model of execution 
was developed by Mantel, Perner and Sauer that is tailored to 
applications in information flow security. In order to increase the 
confidence in this operational model, a machine-checked version of the 
definitions and a clear connection to a well-established model of 
execution are desirable.

This talk presents an Isabelle/HOL formalization of the definitions of 
the operational model of execution and a machine-checked hierarchy 
result with respect to the executions that are possible in this model 
of execution under four exemplary memory models. Furthermore, the talk 
presents some ideas for an adaptation of the operational model of 
execution that aim at making the model comparable to a well-
established axiomatic model of execution. In the future, the 
adaptation shall be completed and a proof skeleton shall be developed 
for the equivalence of the operational and the axiomatic model of 
execution.