Generating Concurrency Checks Automatically. / Hague, Matthew; Hoyland, Jonathan.

Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs . ACM, 2016. p. 1-15 4.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Generating Concurrency Checks Automatically. / Hague, Matthew; Hoyland, Jonathan.

Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs . ACM, 2016. p. 1-15 4.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Hague, M & Hoyland, J 2016, Generating Concurrency Checks Automatically. in Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs ., 4, ACM, pp. 1-15. https://doi.org/10.1145/2955811.2955815

APA

Hague, M., & Hoyland, J. (2016). Generating Concurrency Checks Automatically. In Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs (pp. 1-15). [4] ACM. https://doi.org/10.1145/2955811.2955815

Vancouver

Hague M, Hoyland J. Generating Concurrency Checks Automatically. In Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs . ACM. 2016. p. 1-15. 4 https://doi.org/10.1145/2955811.2955815

Author

Hague, Matthew ; Hoyland, Jonathan. / Generating Concurrency Checks Automatically. Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs . ACM, 2016. pp. 1-15

BibTeX

@inproceedings{ea702ea64c6748e0ad2226998fcb227f,
title = "Generating Concurrency Checks Automatically",
abstract = "This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Action trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata (ATA) that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces ATA that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The ATA produced are easier to scale to large numbers of locks than previous constructions.",
author = "Matthew Hague and Jonathan Hoyland",
year = "2016",
month = jul,
day = "17",
doi = "10.1145/2955811.2955815",
language = "English",
pages = "1--15",
booktitle = "Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs",
publisher = "ACM",

}

RIS

TY - GEN

T1 - Generating Concurrency Checks Automatically

AU - Hague, Matthew

AU - Hoyland, Jonathan

PY - 2016/7/17

Y1 - 2016/7/17

N2 - This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Action trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata (ATA) that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces ATA that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The ATA produced are easier to scale to large numbers of locks than previous constructions.

AB - This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Action trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata (ATA) that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces ATA that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The ATA produced are easier to scale to large numbers of locks than previous constructions.

U2 - 10.1145/2955811.2955815

DO - 10.1145/2955811.2955815

M3 - Conference contribution

SP - 1

EP - 15

BT - Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs

PB - ACM

ER -