Verifying API use of Parallel Programming Models using Contracts
Speaker
Yussur Mustafa Oraji
When
September 10th, 2026 at 2pm
Where
Alan Turing room
Title
Verifying API use of Parallel Programming Models using Contracts
Abstract
Parallel programming models such as MPI and OpenSHMEM facilitate large-scale distributed memory computation, but are low-level, leaving resource management and synchronization to the user. Existing correctness checkers are typically tied to a single programming model, limiting their applicability. To avoid these shortcomings we present CoVer, a verification tool which uses contracts to describe each API's ruleset in a human-readable form. Specifying contracts for a given model extends coverage to new programming models and API functions without requiring a new tool. So far, CoVer can run in static, dynamic, or hybrid analysis modes. We explore the required adaptations to the program at compile- and runtime, with a focus on the difficulties encountered when avoiding hardcoded support for specific programming models. Finally, we discuss the limitations and our current efforts to solve them.