Greg Dennis
Abstract
Two operations commute if executing them serially in either order results in the same change of state. In a system in which commands may be issued simultaneously by different users, lack of commutativity can result in unpredictable behaviour, even if the commands are serialized, because one user's command may be preempted by another's, and thus executed in an unanticipated state. This paper describes an automated approach to analyzing commutativity. The operations are expressed as constraints in a declarative modelling language such as Alloy, and a constraint solver is used to find violating scenarios. A case study application to the beam scheduling component of a proton therapy machine (originally specified in OCL) revealed several violations of commutativity in which requests from medical technicians in treatment rooms could conflict with the actions of a beam operator in a master control room. Some of the issues involved in automating the analysis for OCL itself are also discussed.
- BRAT, G., HAVELUND, K., PARK, S., AND VISSER, W. Java PathFinder - A second generation of a Java modelchecker. In Workshop on Advances in Verification (July 2000).Google Scholar
- CLARK, T., AND WARMER, J., Eds. Object Modeling with the OCL: The Rationale behind the Object Constraint Language. No. 2263 in LNCS. Springer-Verlag, 2002. Google ScholarDigital Library
- FEKETE, A., LYNCH, N., MERRITT, M., AND WEIHL, W. Commutativity-based locking for nested transactions. Journal of Computer and System Sciences 41, 1 (Aug. 1990), 65--156. Google ScholarDigital Library
- FOOD AND DRUG ADMININSTRATION. FDA Statement on Radiation Overexposures in Panama. http://www.fda.gov/cdrh/ocd/panamaradexp.html.Google Scholar
- HOLZMANN, G. J. The Model Checker SPIN. IEEE Transactions on Software Engineering 23, 5 (May 1997), 279--295. Google ScholarDigital Library
- HUSSMANN, H., DEMUTH, B., AND FINGER, F. Modular Architecture for a Toolset Supporting OCL. In Proceedings of UML 2000: Advancing the Standard (York, UK, Oct. 2000), A. Evans, S. Kent, and B. Selic, Eds., no. 1939 in LNCS.Google ScholarCross Ref
- JACKSON, D. Automating First-Order Relational Logic. In Proc. ACM SIGSOFT Conf. Foundations of Software Engineering (FSE) (Nov. 2000). Google ScholarDigital Library
- JACKSON, D., SHLYAKHTER, I., AND SRIDHARAN, M. A micromodularity mechanism. In ACM SIGSOFT Conference on Foundations of Software Engineering / European Software Engineering Conference (Vienna, Sept. 2001). Google ScholarDigital Library
- J.R. BURCH, E.M. CLARKE, K.L. MCMILLAN, D.L. DILL, AND L.J. HWANG. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (Washington, D.C., 1990), IEEE Computer Society Press, pp. 1--33.Google Scholar
- LEVESON, N. G., AND TURNER, C. An investigation of the Therac-25 accidents. IEEE Computer 7, 26 (1993), 18--41. Google ScholarDigital Library
- MCMILLAN, K. L. Symbolic Model Checking. Kluwer Academic Publishers, 1993. http://www.cs.cmu.edu/~modelcheck/smv.html. Google ScholarDigital Library
- MIT SOFTWARE DESIGN GROUP. The Alloy Analyzer. http://alloy.mit.edu.Google Scholar
- QUEILLE, J.-P., AND SIFAKIS, J. Specification and Verification of Concurrent Systems in CESAR. LNCS 137 (1982), 337--351. Google ScholarDigital Library
- RICHTERS, M., AND GOGOLLA, M. OCL: Syntax, Semantics, and Tools. In Clark and Warmer {2}, pp. 42--68. Google ScholarDigital Library
- RICKS, R. C., BERGER, M. E., HOLLOWAY, E. C., AND GOANS, R. E. REACTS Radiation Accident Registry: Update of Accidents in the United States. International Radiation Protection Association, 2000.Google Scholar
- RINARD, M. C., AND DINIZ, P. C. Commutativity analysis: A new analysis technique for parallelizing compilers. ACM Transactions on Programming Languages and Systems 19, 6 (1997), 942--991. Google ScholarDigital Library
- WARMER, J., Ed. Response to the UML 2.0 OCL RfP (ad/2000-09-03). Object Management Group, Jan. 2003. Revised submission, version 1.6. OMG Document ad/2003-01-07.Google Scholar
- WARMER, J., AND KLEPPE, A. The Object Constraint Language: Getting your models ready for MDA, 2nd ed. Addison-Wesley, Aug. 2003. Google ScholarDigital Library
- WEIHL, W. E. Commutativity-based concurrency control for abstract data types. IEEE Transactions on Computers 37, 12 (1988), 1488--1505. Google ScholarDigital Library
- WU, P., AND FEKETE, A. An empirical study of commutativity in application code. In Proceedings of International Database Engineering and Applications Symposium (Hong Kong, July 2003).Google ScholarCross Ref
Index Terms
- Automating commutativity analysis at the design level
Recommendations
Automating commutativity analysis at the design level
ISSTA '04: Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysisTwo operations commute if executing them serially in either order results in the same change of state. In a system in which commands may be issued simultaneously by different users, lack of commutativity can result in unpredictable behaviour, even if ...
Gypsy: A language for specification and implementation of verifiable programs
Proceedings of an ACM conference on Language design for reliable softwareAn introduction to the Gypsy programming and specification language is given. Gypsy is a high-level programming language with facilities for general programming and also for systems programming that is oriented toward communications processing. This ...
SPARE: A Development Environment for Program Analysis Algorithms
A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature ...
Comments