TY - GEN
T1 - Towards static deadlock resolution in the π-calculus
AU - Giunti, Marco
AU - Ravara, António
N1 - sem pdf.
PY - 2014
Y1 - 2014
N2 - Static analysis techniques based on session types discern concurrent programs that ensure the fidelity of protocol sessions - for each input (output) end point of a session there is exactly an output (input) end point available - being expressive enough to represent the standard -calculus and several typing disciplines. More advanced type systems, enforcing properties as deadlock-freedom or even progress, sensibly reduce the set of typed processes, thus mining the expressiveness of the analysis. Herein, we propose a first step towards a compromise solution to this problem: a session based type checking algorithm that releases some deadlocks (when co-actions on the same channel occur in sequence in a thread). This procedure may help the software development process: the typing algorithm detects a deadlock, but instead of rejecting the code, fixes it by looking into the session types and producing new safe code that obeys the protocols and is deadlock-free.
AB - Static analysis techniques based on session types discern concurrent programs that ensure the fidelity of protocol sessions - for each input (output) end point of a session there is exactly an output (input) end point available - being expressive enough to represent the standard -calculus and several typing disciplines. More advanced type systems, enforcing properties as deadlock-freedom or even progress, sensibly reduce the set of typed processes, thus mining the expressiveness of the analysis. Herein, we propose a first step towards a compromise solution to this problem: a session based type checking algorithm that releases some deadlocks (when co-actions on the same channel occur in sequence in a thread). This procedure may help the software development process: the typing algorithm detects a deadlock, but instead of rejecting the code, fixes it by looking into the session types and producing new safe code that obeys the protocols and is deadlock-free.
UR - http://www.scopus.com/inward/record.url?scp=84901298367&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-05119-2_9
DO - 10.1007/978-3-319-05119-2_9
M3 - Conference contribution
AN - SCOPUS:84901298367
SN - 9783319051185
VL - 8358 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 136
EP - 155
BT - Trustworthy Global Computing - 8th International Symposium, TGC 2013, Revised Selected Papers
PB - Springer Verlag
T2 - 8th International Symposium on Trustworthy Global Computing, TGC 2013
Y2 - 30 August 2013 through 31 August 2013
ER -