×

Alias burying: Unique variables without destructive reads. (English) Zbl 1009.68878

Summary: An unshared object can be accessed without regard to possible conflicts with other parts of a system, whether concurrent or single-threaded. A unique variable (sometimes known as a ‘free’ or ‘linear’ variable) is one that either is null or else refers to an unshared object. Being able to declare and check which variables are unique improves a programmer’s ability to avoid program faults.
In previously described uniqueness extensions to imperative languages, a unique variable can be accessed only with a destructive read, which nullifies it after the value is obtained. This approach suffers from several disadvantages: the use of destructive reads increases the complexity of the program which must continually restore nullified values; adding destructive reads changes the semantics of the programming language; and many of the nullifications are actually unnecessary.
We demonstrate instead that uniqueness can be preserved through the use of existing language features. We give a modular static analysis that checks (nonexecutable) uniqueness annotations superimposed on an imperative programming language without destructive reads. The ‘alias-burying intuition’ is that aliases that are ‘dead’ (will never be used again) can be safely ‘buried’ (made undefined).

MSC:

68U99 Computing methodologies and applications
68N15 Theory of programming languages
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

Virginity
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Linear types can change the world! Programming Concepts and Methods, (eds.). Elsevier: North-Holland, 1990.
[2] Hogg, ACM SIGPLAN Notices 26 pp 271– (1991)
[3] Baker, ACM SIGPLAN Notices 30 pp 45– (1995)
[4] Towards alias-free pointers. ECOOP’96 ? Object-Oriented Programming, 10th European Conference, July 8-12, Linz, Austria (Lecture Notes in Computer Science, vol. 1098), (ed.). Springer: Berlin, 1996; 189-209.
[5] Girard, Theoretical Computer Science 50 pp 1– (1987) · Zbl 0625.03037
[6] Harms, IEEE Transactions on Software Engineering 17 pp 424– (1991) · Zbl 05113801
[7] An object-oriented effects system. ECOOP’99?Object-Oriented Programming, 13th European Conference, June 14-18, Lisbon, Portugal (Lecture Notes in Computer Science, vol. 1628), (ed.). Springer: Berlin, 1999; 205-229.
[8] Leino, ACM SIGPLAN Notices 33 pp 144– (1998)
[9] Sagiv, ACM Transactions on Programming Languages and Systems 20 pp 1– (1998) · Zbl 01935724
[10] Syntactic control of interference. Conference Record of the 5th ACM Symposium on Principles of Programming Languages. ACM Press: New York, 1978; 39-46.
[11] Intuitionistic reasoning about shared mutable data structure. Millenial Perspectives in Computer Science. Palgrave, to appear. Draft dated July 2000.
[12] Schmidt, ACM Transactions on Programming Languages and Systems 7 pp 299– (1985) · Zbl 0562.68008
[13] Rolling your own mutable ADT: A connection between linear types and monads. Conference Record of the 24th Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, January 15-17, Paris, France. ACM Press: New York, 1997; 54-66.
[14] Imperative functional programming. Conference Record of the 20th Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, January 10-13, Charleston, SC. ACM Press: New York, 1993; 71-84.
[15] Launchbury, Lisp and Symbolic Computation 8 pp 293– (1995) · Zbl 05478827
[16] Reasoning about aliasing. Proceedings of the 4th Australasian Refinement Workshop (ARW-95). School of Computer Science and Engineering, The University of New South Wales, 1995; 195-211.
[17] High level specification of I/O in functional languages. Workshop on Functional Programming, Glasgow 1992, July 6-8, Ayr, UK, (eds.). Workshops in Computer Science. Springer: Berlin, 1993; 1-17.
[18] Balloon types: Controlling sharing of state in data types. ECOOP’97?Object-Oriented Programming, 11th European Conference, June 9-13, Jyväskylä, Finland (Lecture Notes in Computer Science, vol. 1241). (eds.). Springer: Berlin, 1997; 32-59.
[19] Abstraction and Specification in Program Development. The MIT Press: Cambridge, MA, 1986. · Zbl 0644.68001
[20] Evans, ACM SIGSOFT Software Engineering Notes 19 pp 87– (1994)
[21] Wrestling with rep exposure. SRC Research Report 156, Digital Equipment Corporation, Systems Research Center: Palo Alto, CA, 1998.
[22] Extended static checking. SRC Research Report 159, Compaq Systems Research Center: Palo Alto, CA, 1998.
[23] Leino, Information Processing Letters 70 pp 99– (1999) · Zbl 1002.68025
[24] Flexible alias protection. ECOOP’98?Object-Oriented Programming, 12th European Conference, July 20-24, Brussels, Belgium (Lecture Notes in Computer Science, vol. 1445), (ed.). Springer: Berlin, 1998.
[25] Clarke, ACM SIGPLAN Notices 33 pp 48– (1998)
[26] Promises: Limited specifications for analysis and manipulation. Proceedings of the IEEE International Conference on Software Engineering (ICSE ’98), April 19-25, Kyoto, Japan. IEEE Computer Society: Los Alamitos, CA, 1998; 167-176.
[27] Park, ACM SIGPLAN Notices 26 pp 178– (1991)
[28] Blanchet, ACM SIGPLAN Notices 34 pp 20– (1999)
[29] Whaley, ACM SIGPLAN Notices 34 pp 187– (1999)
[30] Choi, ACM SIGPLAN Notices 34 pp 1– (1999)
[31] Bogda, ACM SIGPLAN Notices 34 pp 35– (1999)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.