Name
Abstract | ||
|---|---|---|
A high-level race occurs when an execution interleaves instructions corresponding to user-annotated critical accesses to shared memory structures. Such races are good indicators of atomicity violations. We propose a technique for detecting all high-level dataraces in a system library like the kernel API of a real-time operating system (RTOS) that relies on flag-based scheduling and synchronization. Our methodology is based on model-checking, but relies on a meta-argument to bound the number of task processes needed to orchestrate a race. We describe our approach in the context of FreeRTOS, a popular RTOS in the embedded domain. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-52234-0_22 | VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2017 |
Field | DocType | Volume |
Kernel (linear algebra),Atomicity,Synchronization,Shared memory,Scheduling (computing),Computer science,Real-time operating system,Operating system,Distributed computing | Conference | 10145 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Suvam Mukherjee | 1 | 2 | 1.09 |
| Arun Kumar | 2 | 0 | 1.01 |
| Deepak D'souza | 3 | 239 | 17.90 |