|Home \ Publications \ InProceedings Page||Login|
Towards static deadlock resolution in the pi calculusAbstract:
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 pi-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.