The “Verification and Validation of Multi-Core System Architectures” Workshop is a one-day in-person seminar within the 2025 IEEE Space Computing Conference(SCC), featuring invited presentations and interactive discussions on best practices for verifying and validating software on a multi-core platform.

The workshop focuses on the transition to multi-core architectures in space flight applications and the resulting implications to a system designer or system integrator’s ability to assess the safety and performance of the architecture under all conditions. It also includes discussion of approaches, engineering methodologies, and tools to enable space flight certification of these systems.

The workshop will be chaired by Alwyn Goodloe (NASA Langley Research Center, Research Computer Engineer), and Scott Tashakkor (NASA/MSFC, NESC Deputy Software Tech Fellow).

The workshop format will include invited presentation and an interactive challenge problem to support discussion amongst audience members

This year we are fortunate to have two distinguished speakers. Dr Samuel R Thompson from Rapita systems who is grappling with the difficulties of assuring safety-critical software implemented in multicore systems that must conform to guidelines and standards used in aerospace. Modern processors allow for more behaviors than traditional sequential consistency by allowing reordering of instructions and relaxing store atomicity. In order to understand and verify the behavior of software running on these processors, one needs a precise understanding of the processor’s memory model. These models are complex and usually poorly documented. Dr. Jade Alglave who leads a team at Arm will tell us about her work on providing precise and both formal definition of the behavior of Arm’s memory model thus improving our ability to verify programs.

Call for Participation

Summary

The “Verification and Validation of Multi-Core System Architectures” Workshop is a one-day in-person seminar within the 2025 IEEE Space Computing Conference(SCC). The workshop format will include invited presentation and an interactive challenge problem to support discussion amongst audience members.

This year we are fortunate to have two distinguished speakers. Dr Samuel R Thompson from Rapita systems who is grappling with the difficulties of assuring safety-critical software implemented in multicore systems that must conform to guidelines and standards used in aerospace. Modern processors allow for more behaviors than traditional sequential consistency by allowing reordering of instructions and relaxing store atomicity. In order to understand and verify the behavior of software running on these processors, one needs a precise understanding of the processor’s memory model. These models are complex and usually poorly documented. Dr. Jade Alglave who leads a team at Arm will tell us about her work on providing precise and both formal definition of the behavior of Arm’s memory model thus improving our ability to verify programs.

Speakers

Speaker: Dr Samuel R Thompson, Multicore Engineering Team Lead, Rapita Systems

Title: Addressing Multicore Interference in Safety- and Mission-Critical Computers

Abstract

—  

Multicore interference can present a significant challenge for computers hosting critical functionality, by allowing independent software executing on different processing cores to affect each other’s timing properties. In the worst case, this interference can cause deadline misses and functional failures. Therefore, it is of great importance to understand (and bound) the impact that multicore interference can have on a given platform.   We discuss some examples of both simple and complex interference channels in space-relevant multicore hardware platforms and present a tooling solution that can be used to support the analysis of interference channels by using a combination of targeted interference generators and measurement tooling.

Dr. Jade Alglave, FREng. ARM and University College London

Title: On formal specifications at Arm

Abstract

The Arm Architecture Formal Team looks after the formalization of a number of areas of the Arm Architecture. Historically, the team has looked after the Concurrency Model, which determines which value a Load instruction is Architecturally Allowed to see. To do that, we develop, maintain and enhance a number of tools which allow us to propose, execute, test and amend formalizations of the prose in the Arm Architecture Reference Manual (Arm ARM). We discuss our proposals with stakeholders and ratify them, after which a (partially automated) transliteration of the formalization lands back into the Arm ARM. The current scope of the model includes some aspects of virtual memory and instruction fetch, and we work assiduously to expand the scope to the entirety of the Architecture.

  More recently, the team has looked into defining and formalizing the Arm Architecture Specification Language (ASL), which is used to describe the behavior of the instructions of the Arm Instruction Set Architecture (ISA). Originally this language was a pseudocode without well defined syntax and semantics, and the team has provided a formal definition of both, as well as a reference interpreter.  

Dr. Alglave will give an overview of her work on both topics, as well as some considerations about the accessibility of specifications, whether formal or not.

Pointers

The formal concurrency model is written in a domain-specific language called cat 1 , which can be interpreted in a tool called herd7 2 . We use the diy7 tool to generate interesting concurrency tests 3, which can be run using the litmus tool 4. The formal definition of ASL can be found at [5[, and the reference interpreter at 6. Various papers show the evolution of the formal Arm concurrency model scope, e.g. 7 and 8.

Schedule

TBD