Verifying concurrent algorithms on Weak Memory Models
Lead Research Organisation:
University of Kent
Department Name: Sch of Computing
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
People |
ORCID iD |
| Scott Owens (Principal Investigator) |
Publications
Ritson C
(2016)
Benchmarking weak memory models
Ritson C
(2016)
Benchmarking weak memory models
in ACM SIGPLAN Notices
Ugawa T
(2018)
Transactional Sapphire Lessons in High-Performance, On-the-fly Garbage Collection
in ACM Transactions on Programming Languages and Systems
| Description | There are three separate developments arising from the research on this award specific to the team at the University of Kent, in addition to their support of the University of Sheffield team. The first is a new approach to studying the weak memory performance of multi-core CPUs. Although there is now extensive work in studying the complex behaviours of multi-core CPUs that are visible to programmers, the interaction between performance and programmability of these devices had not previously considered in depth. The techniques developed here will allow systems programmers (e.g., the developers of Linux and other operating systems, and virtual machines such as the JVM) to analyse their systems and focus their costly weak-memory-related validation efforts (whether formal proof, or extensive testing) on the parts of the system where weak-memory-related implementation decisions have the most effect. (This outcome is part of the follow-on to previous award EP/K040561/1). The second is the software to support running litmus tests for micro-processors that use the ARM architecture. A litmus test is a tiny parallel program designed to determine what kinds of concurrent behaviours a processor can exhibit. There are several hundred of these, and the ability to effectively determine the answers to them underpins all research into the semantics and correctness of concurrent/parallel programs running on modern micro-processors. Litmus testing is challenging because each test might have several outcomes, and the more interesting ones might happen fleetingly rarely, and it is important to establish with some confidence that un-observed results are in fact impossible (although it is impossible to actually prove that). This software aims to solve this problem by making it easy to drive the processor (and memory bus) into various "bad" configurations that make the interesting results more likely to happen. The third is a new mathematical model for describing the behaviour of concurrent programs in a Java-like language. |
| Exploitation Route | This work is of interest to people building key parts of software infrastructure such as operating systems, virtual machines, and compilers. It can help them understand the performance of fundamental parts of their code, and understand better how to reason about its correctness. Other researchers could take up the litmus testing approach and scale it up into a robust testing framework for concurrent software. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Title | Online Litmus Test Analyser |
| Description | This software supports running litmus tests for micro-processors that use the ARM architecture. A litmus test is a tiny parallel program designed to determine what kinds of concurrent behaviours a processor can exhibit. There are several hundred of these, and the ability to effectively determine the answers to them underpins all research into the semantics and correctness of concurrent/parallel programs running on modern micro-processors. Litmus testing is challenging because each test might have several outcomes, and the more interesting ones might happen fleetingly rarely, and it is important to establish with some confidence that un-observed results are in fact impossible (although it is impossible to actually prove that). This software aims to solve this problem by making it easy to drive the processor (and memory bus) into various "bad" configurations that make the interesting results more likely to happen. |
| Type Of Technology | Software |
| Year Produced | 2016 |
| Open Source License? | Yes |
| Impact | The overall goal of the software was to establish that the ARM architecture, in practice, enjoys a nice property (from the perspective of the theory of concurrent programming) called "multi-copy atomicity". ARM's documentation did not promise such a property, but we had never observed its violation in practice. Establishing the property would allow more effective verification of concurrent algorithms by re-purposing known techniques. As the software reached maturity, ARM changed its documentation to guarantee multi-copy atomicity, somewhat obviating the purpose of the software. However, it still can be taken as a starting point for testing larger concurrent programs. |
| URL | https://github.com/SOwens/olta |