Nikita Golovliov: Verification of Multiprocessor System Memory Model

Event Details

In a shared memory multiprocessor system, the memory model determines the outcome of read operations at any time, given a partial order of memory operations induced by processor-issued writes and reads. A memory model may pertain to high-level language semantics or hardware program execution.

This thesis focuses on verification of hardware memory model conformance, i.e. given a hardware specification and memory model, verifying whether all the possible executions of any program on the hardware are permitted by the memory model, and vice versa.

View-based definitions of a memory model require existence of a certain order between memory modification and observation events, called view. If, and only if, there exists a view that is consistent with the memory model for every execution of any program by a multiprocessor system, then the multiprocessor system conforms to the memory model.

Given a generic high-level processor-memory interface, we provide a translation of the release consistency hardware memory model to a set of linear temporal logic properties. We analyse the correctness of the translation and the deficiencies of the approach. We discuss the relation of the hardware memory model to the memory model of C++.

We provide an example multiprocessor system design that is used for verifica- tion of memory model conformance, and the guidelines for applying the properties to a real-world system.