Divyanjali Sharma

dblp:286/8670 · DBLP profile ↗
← Back
3ranked-venue papers
1as first author
3since 2021 · last 2022
0000-0003-1976-6834ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 3 · 1 first-author · 3 since 2021
YearPublicationVenuePosition
2022 Fence Synthesis Under the C11 Memory Model
Sanjana Singh, Divyanjali Sharma, Ishita Jaju, Subodh Sharma 0001
ATVA2
2021 Thread-Modular Analysis of Release-Acquire Concurrency
Divyanjali Sharma, Subodh Sharma 0001
SAS1
2021 Dynamic Verification of C11 Concurrency over Multi Copy Atomics
abstract
We investigate the problem of runtime analysis of concurrent C11 programs under Multi-Copy-Atomic semantics (MCA). Under MCA, one can analyze program outcomes solely through interleaving and reordering of thread events. As a result, obtaining intuitive explanations of program outcomes becomes straightforward. Newer versions of ARM (ARMv8 and later), Alpha, and Intel’s x-86 support MCA. Our tests reveal that state-of-the-art dynamic verification techniques that analyze program executions under the C11 memory model report safety property violations that can be interpreted as false alarms under MCA semantics. Sorting the true from false violations puts an undesirable burden on the user.In this work, we provide a dynamic verification technique (MoCA) to analyze C11 program executions which are permitted under the MCA model. We restrict C11 happens-before relation and propose coherence rules to capture precisely those C11 program executions which are allowed under the MCA model. MoCA’s exploration of the state-space is based on the state-of-the-art dynamic verification algorithm, source-DPOR. Our experiments validate that MoCA captures all coherent C11 program executions, and is precise for the MCA model.
Sanjana Singh, Divyanjali Sharma, Subodh Sharma 0001
TASE2