Comparison of an operational and an axiomatic model of execution for multi-threaded programs 


Relaxed memory consistency models, in contrast to the intuitive 
sequential consistency model, allow the use of modern hardware and 
compiler optimizations. Thereby they non-trivially influence 
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 the original specification of 
the memory models for which it is instantiated are desirable. Since 
other generic models of execution with other areas of application 
exist already, this connection can be achieved through an equivalence 
result between the new model of execution and another generic model 
for which the connection to the original specification of the memory 
models has been established already. The axiomatic model of execution 
by Alglave is suitable for this purpose since it is well-established 
and it has the desired properties with respect to the memory models. 
Since the information that is available in both models is not entirely 
equivalent, adaptations to the new model are required to enable an 
equivalence result.

This talk presents an adapted operational model formalized in 
Isabelle/HOL and a proof outline for the fact that executions which 
are valid in the adapted operational model under the memory models 
Total Store Order (TSO) and Partial Store Order (PSO) are also valid 
in the axiomatic model. These contributions are results of the thesis 
"Comparison of an Operational and an Axiomatic Model of Execution for 
Multi-threaded Programs".

Together with the other results of this thesis, namely a machine-
checked hierarchy result with respect to the executions that are 
possible in the operational model of execution under four exemplary 
memory models and a machine-checked transparency result for the 
adaptations to the operational model of execution, this is the first 
step towards the desired equivalence result between the operational 
and the axiomatic model of execution.