3 papers
cs.LO2025
GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
Soham Chakraborty, S. Krishna, Andreas Pavlogiannis +1
GPU computing is embracing weak memory concurrency for performance improvement. However, compared to CPUs, modern GPUs provide more fine-grained concurrency features such as scopes…
cs.PL2023
On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis +1
Dyck reachability is a principled, graph-based formulation of a plethora of static analyses. Bidirected graphs are used for capturing dataflow through mutable heap data, and are us…
cs.PL2022
Optimal Stateless Model Checking of Transactional Programs under Causal Consistency
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ashutosh Gupta +2
We present a framework for efficient stateless model checking (SMC) of concurrent programs under five prominent models of causal consistency, CCv,CM,CC, Read Committed and Read Ato…