StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities
Proceedings of the ACM on Programming Languages2019Vol. 3(POPL), pp. 1–28
Citations Over TimeTop 10% of 2019 papers
Abstract
We propose and study StkTokens: a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling convention is based on linear capabilities: a type of capabilities that are prevented from being duplicated by the hardware. In addition to designing and formalizing this new calling convention, we also contribute a new way to formalize and prove that it effectively enforces well-bracketed control flow and local state encapsulation using what we call a fully abstract overlay semantics.
Related Papers
- Effectiveness of Thin Hot Mix Asphalt Overlay on Pavement Ride and Condition Performance(2008)
- ASPHALT OVERLAY ON CRACK-SEALED CONCRETE PAVEMENTS USING STRESS DISTRIBUTING MEDIA(1993)
- Selection on Optimum Overlay Thickness for Asphalt Pavement(2005)
- Comparison of Multiprotocol Encapsulation, Unidirectional Lightweight Encapsulation and Generic Stream Encapsulation Protocol(2014)
- PAVEMENT OVERLAY DESIGN PROCEDURES AND ASSUMPTIONS. VOLUME III: GUIDE FOR DESIGNING AN OVERLAY. FINAL REPORT(1986)