Proving Liveness of Parameterized Programs

Azadeh Farzan; Zachary Kincaid; Andreas Podelski

doi:10.1145/2933575.2935310

Proving Liveness of Parameterized Programs

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

27 Scopus citations

Abstract

Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold no matter how many threads are active in the system.

Original language	English (US)
Title of host publication	Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	185-196
Number of pages	12
ISBN (Electronic)	9781450343916
DOIs	https://doi.org/10.1145/2933575.2935310
State	Published - Jul 5 2016
Event	31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - New York, United States Duration: Jul 5 2016 → Jul 8 2016

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Volume	05-08-July-2016
ISSN (Print)	1043-6871

Other

Other	31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
Country/Territory	United States
City	New York
Period	7/5/16 → 7/8/16

All Science Journal Classification (ASJC) codes

Software
General Mathematics

Access to Document

10.1145/2933575.2935310

Cite this

Farzan, A., Kincaid, Z., & Podelski, A. (2016). Proving Liveness of Parameterized Programs. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016 (pp. 185-196). (Proceedings - Symposium on Logic in Computer Science; Vol. 05-08-July-2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/2933575.2935310

@inproceedings{252d2f6084e34b5393d1d98f27519676,

title = "Proving Liveness of Parameterized Programs",

abstract = "Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards {"}the good thing{"} rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold no matter how many threads are active in the system.",

author = "Azadeh Farzan and Zachary Kincaid and Andreas Podelski",

note = "Publisher Copyright: {\textcopyright} 2016 ACM.; 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 ; Conference date: 05-07-2016 Through 08-07-2016",

year = "2016",

month = jul,

day = "5",

doi = "10.1145/2933575.2935310",

language = "English (US)",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "185--196",

booktitle = "Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016",

address = "United States",

}

Farzan, A, Kincaid, Z & Podelski, A 2016, Proving Liveness of Parameterized Programs. in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Proceedings - Symposium on Logic in Computer Science, vol. 05-08-July-2016, Institute of Electrical and Electronics Engineers Inc., pp. 185-196, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, United States, 7/5/16. https://doi.org/10.1145/2933575.2935310

Proving Liveness of Parameterized Programs. / Farzan, Azadeh; Kincaid, Zachary; Podelski, Andreas.
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Institute of Electrical and Electronics Engineers Inc., 2016. p. 185-196 (Proceedings - Symposium on Logic in Computer Science; Vol. 05-08-July-2016).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Proving Liveness of Parameterized Programs

AU - Farzan, Azadeh

AU - Kincaid, Zachary

AU - Podelski, Andreas

PY - 2016/7/5

Y1 - 2016/7/5

N2 - Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold no matter how many threads are active in the system.

AB - Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource, or that all threads eventually agree on a single value. This paper presents a method for proving that such liveness properties hold. Two particular challenges which are addressed in this work are that (1) the correctness argument may rely on global behaviour of the system (e.g., the correctness argument may require that all threads collectively progress towards "the good thing" rather than one thread progressing while the others do not interfere), and (2) such programs are often designed to be executed by any number of threads, and the desired liveness properties must hold no matter how many threads are active in the system.

UR - http://www.scopus.com/inward/record.url?scp=84994613811&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84994613811&partnerID=8YFLogxK

U2 - 10.1145/2933575.2935310

DO - 10.1145/2933575.2935310

M3 - Conference contribution

AN - SCOPUS:84994613811

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 185

EP - 196

BT - Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016

Y2 - 5 July 2016 through 8 July 2016

ER -

Proving Liveness of Parameterized Programs

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this