article

Connecting effects and uniqueness with adoption

Authors:

John Tang Boyland,

William RetertAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 283 - 295

https://doi.org/10.1145/1047659.1040329

Published: 12 January 2005 Publication History

Abstract

"Adoption" is when on piece of stat is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in shared state. In this paper, we give an operational semantics of adoption in a simple procedural language with pointers to records. We define a "permission" type-system that uses adoption to model both effects and uniqueness. We prove type soundness (well-typed programs don't go wrong) and state separation (separately-typed statements cannot access the same state). Then we show how high-level effects and uniqueness annotations can be expressed in the type-system. The distinction between read and write effects is ignored in the body of this paper.

References

[1]

Boyland, J.: The interdependence of effects and uniqueness. Paper from Workshop on Formal Techniques for Java Programs, 2001 (2001).]]

[2]

Hogg, J.: Islands: Aliasing protection in object-oriented languages. In: OOPSLA'91 Conference Proceedings---Object-Oriented Programming Systems, Languages and Applications, New York, ACM Press (1991) 271--285.]]

Digital Library

[3]

Baker, H.G.: 'Use-once' variables and linear objects---storage management, reflection and multi-threading. ACM SIGPLAN Notices (1995) 45--52.]]

Digital Library

[4]

Minsky, N.: Towards alias-free pointers. In Cointe, P., ed.: ECOOP'96 --- Object-Oriented Programming, 10th European Conference. Volume 1098 of Lecture Notes in Computer Science., Berlin, Heidelberg, New York, Springer (1996) 189--209.]]

Digital Library

[5]

Aldrich, J., Kostadinov, V., Chambers, C.: Alias annotations for program understanding. In: OOPSLA'02 Conference Proceedings---Object-Oriented Programming Systems, Languages and Applications, New York, ACM Press (2002) 311--330.]]

Digital Library

[6]

Clarke, D., Wrigstad, T.: External uniqueness. In Pierce, B.C., ed.: Informal Proceedings of International Workshop on Foundations of Object-Oriented Languages 2003 (FOOL 10). (2003).]]

[7]

DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proceedings of the ACM SIGPLAN '01 Conference on Programming Language Design and Implementation, New York, ACM Press (2001) 59--69.]]

Digital Library

[8]

Fähndrich, M., DeLine, R.: Adoption and focus: Practial linear types for imperative programming. In: Proceedings of the ACM SIGPLAN '02 Conference on Programming Language Design and Implementation, New York, ACM Press (2002) 13--24.]]

Digital Library

[9]

Leino, K.R.M., Stata, R.: Virginity: A contribution to the specification of object-oriented software. Information Processing Letters (1999) 99--105.]]

Digital Library

[10]

Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. Research Report 160, Compaq Systems Research Center, Palo Alto, California, USA (2000).]]

[11]

Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Proceedings of the ACM SIGPLAN '02 Conference on Programming Language Design and Implementation, New York, ACM Press (2002) 246--257.]]

Digital Library

[12]

Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales, Sydney, Australia (2001).]]

Digital Library

[13]

Müller, P.: Modular Specification and Verification of Object-Oriented Programs. PhD thesis, Fernuniversität Hagen (2001).]]

[14]

Boyland, J.: Alias burying: Unique variables without destructive reads. Software Practice and Experience (2001) 533--553.]]

Digital Library

[15]

Greenhouse, A., Boyland, J.: An object-oriented effects system. In Guerraoui, R., ed.: ECOOP'99 --- Object-Oriented Programming, 13th European Conference. Volume 1628 of Lecture Notes in Computer Science., Berlin, Heidelberg, New York, Springer (1999) 205--229.]]

Digital Library

[16]

Boyland, J.: Checking interference with fractional permissions. In Cousot, R., ed.: Static Analysis: 10th International Symposium. Volume 2694 of Lecture Notes in Computer Science., Berlin, Heidelberg, New York, Springer (2003) 55--72.]]

Digital Library

[17]

Leino, K.R.M.: Data groups: Specifying the modification of extended state. In: OOPSLA'98 Conference Proceedings---Object-Oriented Programming Systems, Languages and Applications, New York, ACM Press (1998) 144--153.]]

Digital Library

[18]

Xi, H.: Dependent Types in Practical Programming. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA (1998).]]

Digital Library

[19]

O'Hearn, P., Pym, D.: The logic of bunched implications. Bulletin of Symbolic Logic (1999) 215--244.]]

[20]

Ishtiaq, S.S., O'Hearn, P.W.: BI as an assertion language for mutable data structures. In: Conference Record of the Twenty-eighth Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, New York, ACM Press (2001) 14--26.]]

Digital Library

[21]

O'Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Conference Record of POPL 2004: the 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, New York, ACM Press (2004) 268--280.]]

Digital Library

[22]

Bruce, K.C., Cardelli, L., Pierce, B.C.: Comparing object encodings. In: Theoretical Aspects of Computer Software. Volume 1281 of Lecture Notes in Computer Science. Springer, Berlin, Heidelberg, New York (1997) 415--438.]]

Digital Library

[23]

Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA'03 Conference Proceedings---Object-Oriented Programming Systems, Languages and Applications, New York, ACM Press (2003) 302--312.]]

Digital Library

[24]

Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN '02 Conference on Programming Language Design and Implementation, New York, ACM Press (2002) 1--12.]]

Digital Library

[25]

Fähndrich, M., Leino, K.R.M.: Heap monotonic typestates. In: Informal Proceedings of "International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO)", Utrecht University, Netherlands (2003).]]

[26]

Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Types in Compilation: Third International Workshop, TIC 2000. Volume 2071 of Lecture Notes in Computer Science., Berlin, Heidelberg, New York, Springer (2001) 177--206.]]

Digital Library

[27]

Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, Los Alamitos, California, IEEE Computer Society (2002) 55--74.]]

Digital Library

[28]

Smith, F., Walker, D., Morrisett, J.G.: Alias types. In Smolka, G., ed.: ESOP'00 --- Programming Languages and Systems, 9th European Symposium on Programming. Volume 1782 of Lecture Notes in Computer Science., Berlin, Heidelberg, New York, Springer (2000) 366--381.]]

Digital Library

[29]

Tofte, M., Talpin, J.P.: Implementation of the typed call-by-value λ-calculus using a stack of regions. In: Conference Record of the Twenty-first Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages, New York, ACM Press (1994) 188--201.]]

Digital Library

[30]

Walker, D., Crary, K., Morrisett, G.: Typed memory management via static capabilities. ACM Transactions on Programming Languages and Systems (2000) 701--771.]]

Digital Library

[31]

Monnier, S.: Typed regions. In: Informal Proceedings of "Second workshop on Semantics, Program Analysis, And Computing Environments For Memory Management", University of Copenhagen (2004).]]

[32]

Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, L'Université Paris VII (1994).]]

[33]

Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: preventing data races and deadlocks. In: OOPSLA'02 Conference Proceedings---Object-Oriented Programming Systems, Languages and Applications, New York, ACM Press (2002) 211--230.]]

Digital Library

[34]

Boyapati, C., Salcianu, A., Beebee, W., Rinard, M.: Ownership types for safe region-based memory management in real-time java. In: Proceedings of the ACM SIGPLAN '03 Conference on Programming Language Design and Implementation, New York, ACM Press (2003) 324--337.]]

Digital Library

Cited By

Faes MGross T(2019)Parallel Roles for Practical Deterministic Parallel ProgrammingLanguages and Compilers for Parallel Computing10.1007/978-3-030-35225-7_12(163-181)Online publication date: 15-Nov-2019
https://doi.org/10.1007/978-3-030-35225-7_12
Charguéraud APottier F(2017)Temporary Read-Only Permissions for Separation LogicProgramming Languages and Systems10.1007/978-3-662-54434-1_10(260-286)Online publication date: 19-Mar-2017
https://doi.org/10.1007/978-3-662-54434-1_10
Benitez SMurray TStefan D(2016)Short PaperProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993604(69-75)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993604
Show More Cited By

Index Terms

Connecting effects and uniqueness with adoption
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Connecting effects and uniqueness with adoption
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

"Adoption" is when on piece of stat is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in ...
Electronic business adoption by European firms: a cross-country assessment of the facilitators and inhibitors
Managing e-business transformation

In this study, we developed a conceptual model for studying the adoption of electronic business (e-business or EB) at the firm level, incorporating six adoption facilitators and inhibitors, based on the technology-organization-environment theoretical ...
Adoption of software as a service in Indonesia

We investigate the influence of organizational factors on the adoption og software as a service (SaaS) in Indonesian companies.Our findings on organizational size and organizational readiness contradict the extant literature.Theory regarding information ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
527
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)2

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Faes MGross T(2019)Parallel Roles for Practical Deterministic Parallel ProgrammingLanguages and Compilers for Parallel Computing10.1007/978-3-030-35225-7_12(163-181)Online publication date: 15-Nov-2019
https://doi.org/10.1007/978-3-030-35225-7_12
Charguéraud APottier F(2017)Temporary Read-Only Permissions for Separation LogicProgramming Languages and Systems10.1007/978-3-662-54434-1_10(260-286)Online publication date: 19-Mar-2017
https://doi.org/10.1007/978-3-662-54434-1_10
Benitez SMurray TStefan D(2016)Short PaperProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993604(69-75)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993604
Castegren EÖstlund JWrigstad T(2015)Refined Ownership:Formal Methods for Multicore Programming10.1007/978-3-319-18941-3_5(179-210)Online publication date: 7-May-2015
https://doi.org/10.1007/978-3-319-18941-3_5
Pezzè MWuttke J(2009)Automatic Generation of Runtime Failure Detectors from Property TemplatesSoftware Engineering for Self-Adaptive Systems10.1007/978-3-642-02161-9_12(223-240)Online publication date: 10-Jun-2009
https://dl.acm.org/doi/10.1007/978-3-642-02161-9_12
Saffrich HNishida YThiemann P(2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689763
Gonnord LHenrio LMorel LRadanne G(2023)A Survey on Parallelism and DeterminismACM Computing Surveys10.1145/356452955:10(1-28)Online publication date: 2-Feb-2023
https://dl.acm.org/doi/10.1145/3564529
Milano MTurcotti JMyers AJhala RDillig I(2022)A flexible type system for fearless concurrencyProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523443(458-473)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523443
Radanne GSaffrich HThiemann P(2020)Kindly bent to free usProceedings of the ACM on Programming Languages10.1145/34089854:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408985
Darvariu VConvertino LMehrotra AMusolesi M(2020)Quantifying the Relationships between Everyday Objects and Emotional States through Deep Learning Based Image Analysis Using SmartphonesProceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies10.1145/33809974:1(1-21)Online publication date: 18-Mar-2020
https://dl.acm.org/doi/10.1145/3380997
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents