- Autori:
-
Ernst, Michael D.; Lovato, Alberto; Macedonio, Damiano; Spoto, Fausto; Thaine, Javier
- Titolo:
-
Locking Discipline Inference and Checking
- Anno:
-
2016
- Tipologia prodotto:
-
Contributo in atti di convegno
- Tipologia ANVUR:
- Contributo in Atti di convegno
- Lingua:
-
Inglese
- Formato:
-
A Stampa
- Titolo del Convegno:
- The 38th International Conference on Software Engineering
- Luogo:
- Austin, Texas
- Periodo:
- 2016
- Casa editrice:
- ACM
- ISBN:
- 978-1-4503-3900-1
- Intervallo pagine:
-
1133-1144
- Parole chiave:
-
Static Analysis, concurrent programs, multithreaded programs
- Breve descrizione dei contenuti:
- Concurrency is a requirement for much modern software, but the implementation of multithreaded algorithms comes at the risk of errors such as data races. Programmers can prevent data races by documenting and obeying a locking discipline, which indicates which locks must be held in order to access which data. This paper introduces a formal semantics for locking specifications that gives a guarantee of race freedom. The paper also provides two implementations of the formal semantics for the Java language: one based on abstract interpretation and one based on type theory. To the best of our knowledge, these are the first tools that can soundly infer and check a locking discipline for Java. Our experiments com-pare the implementations with one another and with annotations written by programmers.
- Id prodotto:
-
91245
- Handle IRIS:
-
11562/937422
- ultima modifica:
-
25 dicembre 2019
- Allegati:
- 1
- Citazione bibliografica:
-
Ernst, Michael D.; Lovato, Alberto; Macedonio, Damiano; Spoto, Fausto; Thaine, Javier,
Locking Discipline Inference and Checking
in Proceedings of the 38th International Conference on Software Engineering
,
ACM
,
Atti di "The 38th International Conference on Software Engineering"
, Austin, Texas
, 2016
,
2016
,
pp. 1133-1144
Consulta la scheda completa presente nel
repository istituzionale della Ricerca di Ateneo 
