![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Friday 23 October 2020, 14:00-15:00
Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Symbolic Execution
- đ¤ Speaker: Alasdair Armstrong, University of Cambridge đ Website
- đ Date & Time: Friday 23 October 2020, 14:00 - 15:00
- đ Venue: Online
Abstract
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.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- Online
- School of Technology
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.