Contextual effects for version-consistent dynamic software updating and safe concurrent programming

ABSTRACT

This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we computethe effect of the computation that has already occurred(the prior effect) and the effect of the computation yet to take place (the future effect).

Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency(TVC), a novel correctness property for dynamic software updates. TV Censures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.

REFERENCES

• 1: Martin Abadi and Cedric Fournet. Access control based on execution history. In NDSS, 2003.
• 2: Andrew Baumann , Gernot Heiser , Jonathan Appavoo , Dilma Da Silva , Orran Krieger , Robert W. Wisniewski , Jeremy Kerr, Providing dynamic update in an operating system, Proceedings of the annual conference on USENIX Annual Technical Conference, p.32-32, April 10-15, 2005, Anaheim, CA
• 3: Andrew Baumann , Jonathan Appavoo , Robert W. Wisniewski , Dilma Da Silva , Orran Krieger , Gernot Heiser, Reboots are for hardware: challenges and solutions to updating an operating system on the fly, 2007 USENIX Annual Technical Conference on Proceedings of the USENIX Annual Technical Conference, p.1-14, June 17-22, 2007, Santa Clara, CA
• 4: Chandrasekhar Boyapati , Barbara Liskov , Liuba Shrira , Chuang-Hue Moh , Steven Richman, Lazy modular upgrades in persistent object stores, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 5: Haibo Chen , Rong Chen , Fengzhe Zhang , Binyu Zang , Pen-Chung Yew, Live updating operating systems using virtualization, Proceedings of the 2nd international conference on Virtual execution environments, June 14-16, 2006, Ottawa, Ontario, Canada [doi>10.1145/1134760.1134767]
• 6: Haibo Chen , Jie Yu , Rong Chen , Binyu Zang , Pen-Chung Yew, POLUS: A POwerful Live Updating System, Proceedings of the 29th international conference on Software Engineering, p.271-281, May 20-26, 2007 [doi>10.1109/ICSE.2007.65]
• 7: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 8: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 9: Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006 [doi>10.1145/1186632.1186635]
• 10: Stephen Gilmore, Dilsun Kirli, and Chris Walton. Dynamic ML without dynamic types. Technical Report ECS-LFCS-97-378, LFCS, University of Edinburgh, 1997.
• 11: Tim Harris , Keir Fraser, Language support for lightweight transactions, Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, October 26-30, 2003, Anaheim, California, USA
• 12: Maurice Herlihy , J. Eliot B. Moss, Transactional memory: architectural support for lock-free data structures, Proceedings of the 20th annual international symposium on Computer architecture, p.289-300, May 16-19, 1993, San Diego, California, United States
• 13: Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Lock Inference for Atomic Sections. In TRANSACT, 2006.
• 14: Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.331-342, January 16-18, 2002, Portland, Oregon
• 15: John Kodumal and Alexander Aiken. Banshee: A scalable constraint-based analysis toolkit. In SAS, 2005.
• 16: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 17: Insup Lee, Dymos: a dynamic modification system, The University of Wisconsin - Madison, 1983
• 18: John M. Lucassen. Types and Effects: Towards the Integration of Functional and Imperative Programming. PhD thesis, MIT Laboratory for Computer Science, August 1987. MIT/LCS/TR-408.
• 19: Kristis Makris , Kyung Dong Ryu, Dynamic and adaptive updates of non-quiescent subsystems in commodity operating system kernels, Proceedings of the 2nd ACM SIGOPS/EuroSys European Conference on Computer Systems 2007, March 21-23, 2007, Lisbon, Portugal
• 20: Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-391, January 12-14, 2005, Long Beach, California, USA
• 21: John C. Mitchell. Type inference with simple subtypes. JFP, 1(3):245--285, July 1991.
• 22: Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 23: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 24: Iulian Neamtiu , Jeffrey S. Foster , Michael Hicks, Understanding source code evolution using abstract syntax tree matching, Proceedings of the 2005 international workshop on Mining software repositories, p.1-5, May 17-17, 2005, St. Louis, Missouri
• 25: Iulian Neamtiu , Michael Hicks , Gareth Stoyle , Manuel Oriol, Practical dynamic software updating for C, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 26: Iulian Neamtiu, Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Contextual Effects for Version-Consistent Dynamic Software Updating and Safe Concurrent Programming. Technical Report CS-TR-4920, Dept. of Computer Science, University of Maryland, November 2007.
• 27: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 28: Yang Ni , Vijay S. Menon , Ali-Reza Adl-Tabatabai , Antony L. Hosking , Richard L. Hudson , J. Eliot B. Moss , Bratin Saha , Tatiana Shpeisman, Open nesting in software transactional memory, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming, March 14-17, 2007, San Jose, California, USA [doi>10.1145/1229428.1229442]
• 29: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 30: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 31: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.27-37, October 05-08, 1997, Saint Malo, France
• 32: Christian Skalka , Scott Smith , David Van horn, Types and trace effects of higher order programs, Journal of Functional Programming, v.18 n.2, p.179-249, March 2008 [doi>10.1017/S0956796807006466]
• 33: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 34: Craig AN. Soules, Jonathan Appavoo, Kevin Hui, et al. System support for online reconfiguration. In USENIX, 2003.
• 35: Gareth Stoyle , Michael Hicks , Gavin Bierman , Peter Sewell , Iulian Neamtiu, Mutatis Mutandis: Safe and predictable dynamic software updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.4, p.22-es, August 2007 [doi>10.1145/1255450.1255455]
• 36: Christoph von Praun , Thomas R. Gross, Static conflict analysis for multi-threaded object-oriented programs, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 37: David Walker , Karl Crary , Greg Morrisett, Typed memory management via static capabilities, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.4, p.701-771, July 2000 [doi>10.1145/363911.363923]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Reliability, availability, and serviceability

  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

General Terms:
Languages, Reliability, Theory, Verification

Keywords:
computation effects, contextual effects, data race detection, dynamic software updating, type and effect systems, version consistency