Checking Concurrency Coding Rules
We present an approach for checking that Java programs correctly use libraries such as java.util.concurrent.locks for synchronizing concurrent tasks. Concretely, the article develops methods to check that the behaviour of a program is in accordance with a set of coding rules that govern the correct usage of the library. Here such coding rules are formalized as Prolog predicates that judge whether the history of interactions between program and library is permitted by the rule or not. The history of interactions is obtained by tracing the interactions between the program and the library when executing a representative test suite. The approach is evaluated in a case study where around two hundred independent monitor-based Java implementations of a common specification are analysed to check adherence to the concurrency coding rules.
Mon 20 JanDisplayed time zone: Mountain Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs PADL Felipe Gorostiaga IMDEA Software Institute, Martin Ceresa IMDEA Software Institute, César Sánchez IMDEA Software Institute | ||
16:30 30mTalk | Checking Concurrency Coding Rules PADL Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid | ||
17:00 10mTalk | Can Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk) PADL Michael Hanus Kiel University | ||
17:10 10mTalk | Logic Programming with Extensible Types (Lightning talk) PADL Ivan Perez NASA Ames Research Center, Ángel Herranz Universidad Politécnica de Madrid, P: Julio Mariño Universidad Politécnica de Madrid |