Analyzing singularity channel contracts

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Analyzing singularity channel contracts

Full text

Pdf (493 KB)

Source

International Symposium on Software Testing and Analysis archive
Proceedings of the eighteenth international symposium on Software testing and analysis table of contents

Chicago, IL, USA

SESSION: Static analysis and verification table of contents

Pages 13-24

Year of Publication: 2009

ISBN:978-1-60558-338-9

Authors

Zachary Stengel	University of California at Santa Barbara, Santa Barbara, CA, USA
Tevfik Bultan	University of California at Santa Barbara, Santa Barbara, CA, USA

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering
SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 47, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1572272.1572275 What is a DOI?

ABSTRACT

This paper presents techniques for analyzing channel contract specifications in Microsoft Research's Singularity operating system. A channel contract is a state machine that specifies the allowable interactions between a server and a client through an asynchronous communication channel. We show that, contrary to what is claimed in the Singularity documentation, processes that faithfully follow a channel contract can deadlock. We present a realizability analysis that can be used to identify channel contracts with problems. Our realizability analysis also leads to an efficient verification approach where properties about the interaction behavior can be verified without modeling the contents of communication channels. We analyzed more than 90 channel contracts from the Singularity code distribution and documentation. Only two contracts failed our realizability condition and these two contracts allow deadlocks. Our experimental results demonstrate that realizability analysis and verification of channel contracts can be done efficiently using our approach.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Leslie Lamport , Pierre Wolper, Realizable and Unrealizable Specifications of Reactive Systems, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.1-17, July 11-15, 1989
	2	Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Realizability and Verification of MSC Graphs, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.797-808, July 08-12, 2001
	3	Tevfik Bultan , Xiang Fu , Richard Hull , Jianwen Su, Conversation specification: a new approach to design and analysis of e-service composition, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775210]
	4	Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
	5	Xiang Fu , Tevfik Bultan , Jianwen Su, Conversation protocols: a formalism for specification and verification of reactive electronic services, Theoretical Computer Science, v.328 n.1-2, p.19-37, 29 November 2004 [doi>10.1016/j.tcs.2004.07.004]
	6	X. Fu, T. Bultan, and J. Su. WSAT: A tool for formal analysis of web services. In Proc. 16th Int. Conf. on Computer Aided Verification, pages 510--514, 2004.
	7	Xiang Fu , Tevfik Bultan , Jianwen Su, Synchronizability of Conversations among Web Services, IEEE Transactions on Software Engineering, v.31 n.12, p.1042-1055, December 2005 [doi>10.1109/TSE.2005.141]
	8	Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003
	9	Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
	10	Kohei Honda , Nobuko Yoshida , Marco Carbone, Multiparty asynchronous session types, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
	11	Galen C. Hunt , James R. Larus, Singularity: rethinking the software stack, ACM SIGOPS Operating Systems Review, v.41 n.2, p.37-49, April 2007 [doi>10.1145/1243418.1243424]
	12	Message Sequence Chart (MSC). ITU-T, Geneva Recommendation Z.120, 1994.
	13	A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75293]
	14	Amir Pnueli , Roni Rosner, On the Synthesis of an Asynchronous Reactive Module, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.652-671, July 11-15, 1989
	15	Singularity design note 5: Channel contracts. singularity rdk documentation (v1.1). http://www.codeplex.com/singularity, 2004.
	16	Sebastian Uchitel , Jeff Kramer , Jeff Magee, Incremental elaboration of scenario-based specifications and behavior models using implied scenarios, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.1, p.37-85, January 2004 [doi>10.1145/1005561.1005563]