Pubblicazioni

Autori:

Ernst, Michael D.; Lovato, Alberto; Macedonio, Damiano; Spoto, Nicola 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:

International Conference on Software Engineering (ICSE)

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:

11 novembre 2022

Citazione bibliografica:

Ernst, Michael D.; Lovato, Alberto; Macedonio, Damiano; Spoto, Nicola Fausto; Thaine, Javier, Locking Discipline Inference and Checking  in Proceedings of the 38th International Conference on Software Engineering (ICSE) , ACM , Atti di "International Conference on Software Engineering (ICSE)" , Austin, Texas , 2016 , 2016 , pp. 1133-1144

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo