Abstract
We present a type-based technique for the verification of deadlock-freedom in asynchronous concurrent systems. Our general approach is to start with a simple interaction category, in which objects are types containing safety specifications and morphisms are processes. We then use a specification structure to add information to the types so that they specify stronger properties. In this paper the starting point is the category ASProc and the extra type information concerns deadlock-freedom. In the resulting category ASPrOC D , combining well-typed processes preserves deadlock-freedom. It is also possible to accommodate non-compositional methods within the same framework. The systems we consider are asynchronous, hence issues of divergence become significant; our approach incorporates an elegant treatment of both divergence and successful termination. As an example, we use our methods to verify the deadlock-freedom of an implementation of the alternating-bit protocol.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky, S. J. Gay, and R. Nagarajan. Interaction categories and foundations of typed concurrent programming. In M. Broy, editor, Deductive Program Design: Proceedings of the 1994 Marktoberdorf International Summer School, NATO ASI Series F: Computer and Systems Sciences. Springer-Verlag, 1995.
S. Abramsky, S. J. Gay, and R. Nagarajan. Specification structures and propositions-as-types for concurrency. In G. Birtwistle and F. Moller, editors, Logics for Concurrency: Structure vs. Automata—Proceedings of the VIIIth Banff Higher Order Workshop, volume 1043 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
S. Abramsky. Interaction Categories and communicating sequential processes. In A. W. Roscoe, editor, A Classical Mind: Essays in Honour of C. A. R. Hoare, pages 1–15. Prentice Hall International, 1994.
L. Aceto and M. Hennessy. Termination, deadlock and divergence. Journal of the ACM, 39:147–187, January 1992.
M. Barr. *-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159–178, July 1991.
M. Berger, S. Gay, and R. Nagarajan. A typed calculus of deadlock-free processes. Paper in preparation, 1997.
S. D. Brookes and A. W. Roscoe. Deadlock analysis in networks of communicating processes. In K. Apt, editor, Logics and Models of Concurrent Systems, volume 13, pages 305–324. NATO Advanced Study Institutes, Series F, Springer-Verlag, Berlin, 1985.
K. M. Chandy and J. Misra. Deadlock absence proofs for networks of communicating processes. Information Processing Letters, 9(4), November 1979.
J. W. de Bakker. Mathematical Theory of Program Correctness. Prentice Hall International, 1980.
E. W. Dijkstra and C. S. Scholten. A class of simple communication patterns. In Selected Writings on Computing. EWD643. Springer-Verlag, 1982.
S. J. Gay. Linear Types for Communicating Processes. PhD thesis, University of London, 1995.
S. J. Gay and R. Nagarajan. A typed calculus of synchronous processes. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1995.
J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1–102, 1987.
R. Hoofman. Non-Standard Models of Linear Logic. PhD thesis, Universiteit Utrecht, Netherlands, 1992.
N. Kobayashi. A partially deadlock-free typed process calculus. In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1997.
N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. In Proceedings, 23rd ACM Symposium on Principles of Programming Languages, 1996.
S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.
J. McKinna and R. Burstall. Deliverables: A categorical approach to program development in type theory. In Proceedings of Mathematical Foundation of Computer Science, 1993.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
R. Nagarajan. Typed Concurrent Programs: Specification & Verification. PhD thesis, University of London, 1997. To appear.
P. W. O'Hearn and R. D. Tennent. Relational parametricity and local variables. In Proceedings, 20th ACM Symposium on Principles of Programming Languages. ACM Press, 1993.
S. S. Owicki and D. Cries. Verifying properties of parallel programs. Communications of the ACM, 19(5):279–285, May 1976.
A. M. Pitts. Relational properties of recursively defined domains. In 8th Annual Symposium on Logic in Computer Science, pages 86–97. IEEE Computer Society Press, Washington, 1993.
A. W. Roscoe and N. Daithi. The pursuit of deadlock freedom. Information and Computation, 75(3):289–327, December 1987.
J. Sifakis. Deadlocks and livelocks in transition systems. In Mathematical Foundations of Computer Science, volume 88 of Lecture Notes in Computer Science, pages 587–599. Springer-Verlag, Berlin, 1980.
K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. In Proceedings of the 6th European Conference on Parallel Languages and Architectures, number 817 in Lecture Notes in Computer Science. Springer-Verlag, 1994.
W. W. Wadge. An extensional treatment of dataflow deadlock. Theoretical Computer Science, 13:3–15, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abramsky, S., Gay, S., Nagarajan, R. (1997). A type-theoretic approach to deadlock-freedom of asynchronous systems. In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014557
Download citation
DOI: https://doi.org/10.1007/BFb0014557
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive