Reasoning About a Machine with Local Capabilities: Provably Safe Stack\n and Return Pointer Management - Technical Appendix Including Proofs and\n Details

2019/02/14 by Lau Skorstengaard, Skorstengaard, Lau, Dominique Devriese +3
Computer Science · #Parallel Computing and Optimization Techniques #Computability, Logic, AI Algorithms #Distributed systems and fault tolerance

paper · pdf · doi:10.48550/arxiv.1902.05283

Abstract

We propose a calling convention for capability machines with local\ncapabilities. The calling convention ensures local-state encapsulation and\nwell-bracketed control flow. We use the calling convention in a hand-full of\nprogram examples and prove that they behave correctly. The correctness proofs\nuse a logical relation that is also presented in this appendix. This is the\ntechnical appendix for the paper with the same name and authors accepted at\nESOP18 and under review for TOPLAS.\n

Related

• StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
• Local Reasoning about Parametric and Reconfigurable Component-based Systems
• Uninitialized Capabilities
• Locally Solvable Tasks and the Limitations of Valency Arguments
• Scope Logic with Local Reasoning and Pre/Post-State Properties