University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Symbolic Execution

Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Symbolic Execution

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jamie Vicary.

In this talk I will present work on an in-progress tool for simulating relaxed memory models over the full ARMv8-A architecture. Using symbolic execution of Sail instruction set architecture specifications, and in particular a translation of ARM ’s ASL specification, this tool allows us to simulate the concurrent behavior of litmus tests spanning the entire architecture. As an illustrative example, we can consider how the instruction cache maintenance instructions interact with self-modifying code in an axiomatic setting, or the weak-memory behavior of page table updates. Such behavior is relevant for the semantics of systems software like operating systems and hypervisors which routinely interact with such architectural features in a concurrent way.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity