Promising ARMv8/RISC-V relaxed memory

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

• Christopher Pulte, University of Cambridge
• Friday 29 January 2021, 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

For ARMv8 and RISC -V, there are concurrency models in two styles: axiomatic models, expressing the concurrency semantics in terms of global properties of complete executions; and operational models, that compute incrementally. The latter are in an abstract microarchitectural style: they execute each instruction in multiple steps, out-of-order and with explicit branch speculation. This similarity to hardware implementations has been important in developing the models and in establishing confidence, but involves complexity that, for programming and model-checking, one would prefer to avoid.

We present new equivalent, more abstract operational models for ARMv8 and RISC -V, and an exploration tool based on them. The models compute the allowed concurrency behaviours incrementally based on thread-local conditions and are significantly simpler than the existing operational models: executing instructions in a single step and (with the exception of early writes) in program order, and without branch speculation. The exploration tool is fast enough for exhaustively checking the concurrency behaviour of a number of interesting examples. We use the tool for checking several standard concurrent datastructure and lock implementations, and for interactively stepping through model-allowed executions for debugging.

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
• yk373's list

Note that ex-directory lists are not shown.