Name
Abstract | ||
|---|---|---|
Today, numerous elaborate algorithms for the effective synchronization of concurrent processes operating on shared memory exist. Of particular importance for the verification of such concurrent algorithms are thread-local proof techniques, which allow to reason about the sequential program of one process individually. While thread-local verification of safety properties has received a lot of attention in recent years, this is less so for liveness properties, in particular for liveness under the assumption of fairness. In this paper, we propose a new thread-local proof technique for starvation freedom. Starvation freedom states that under a weakly fair schedule every process will eventually make progress. We contrast our new proof technique with existing global proof techniques based on ranking functions, and employ it exemplarily for the proof of starvation freedom of ticket locks, the standard locking algorithm of the Linux kernel. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-33693-0_13 | IFM |
Field | DocType | Volume |
Synchronization,Ranking,Shared memory,Computer science,Critical section,Ticket,Theoretical computer science,Thread (computing),Liveness,Linux kernel,Distributed computing | Conference | 9681 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
15 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerhard Schellhorn | 1 | 769 | 56.43 |
| Oleg Travkin | 2 | 52 | 5.66 |
| Heike Wehrheim | 3 | 1013 | 104.85 |