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

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

• Alasdair Armstrong, University of Cambridge
• Friday 23 October 2020, 14:00-15:00
• Online.

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

https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU16aG9wdz09

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Online
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.