University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Promising ARMv8/RISC-V relaxed memory

Promising ARMv8/RISC-V relaxed memory

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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