| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
Analyzing Conflict Freedom For Multi-threaded Programs With Time Annotations
Abstract : Avoiding access conflicts is a major challenge in the design of multi-threaded programs. In the context of real-time systems, the absence of conflicts can be guaranteed by ensuring that no two potentially conflicting accesses are ever scheduled concurrently.In this paper, we analyze programs that carry time annotations specifying the time for executing each statement. We propose a technique for verifying that a multi-threaded program with time annotations is free of access conflicts. In particular, we generate constraints that reflect the possible schedules for executing the program and the required properties. We then invoke an SMT solver in order to verify that no execution gives rise to concurrent conflicting accesses. Otherwise, we obtain a trace that exhibits the access conflict.
Cited literature [19 references]
https://hal.inria.fr/hal-01087871
Contributor : Stephan Merz <>
Submitted on : Thursday, November 27, 2014 - 2:41:07 AM
Last modification on : Tuesday, May 19, 2020 - 3:52:41 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:16:36 AM
Contributor : Stephan Merz <>
Submitted on : Thursday, November 27, 2014 - 2:41:07 AM
Last modification on : Tuesday, May 19, 2020 - 3:52:41 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:16:36 AM
Files
postproceedings.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License