TAILIEUCHUNG - Permission Accounting in Separation Logic

Calculation of disposal costs may involve a set of tasks. It may be necessary to calculate material flows (an engineering exercise) from the plant's production process so that wastes can be desegregated and tracked. These material flows will then have to be translated into disposal costs. This calculation can be complex. Consider the issues that arise if the waste is destined for landfill disposal. First, there will be marginal disposal costs associated with transport of the waste. Second, the waste's contribution to landfill costs must be calculated. If a third-party landfiller is to be used, costs will include the. | Permission Accounting in Separation Logic Richard Bornat School of Computing Science Middlesex University LONDON N17 8HR Uk Peter O Hearn Department of Computer Science Queen Mary University of London LONDON E1 4NS UK ohearn@ Cristiano Calcagno Department of Computing Imperial College University of London LONDON SW7 2AZ UK ccris@ Matthew Parkinson Computer Laboratory University of Cambridge CAMBRIDGE CB3 0FD UK mjp41@ ABSTRACT A lightweight logical approach to race-free sharing of heap storage between concurrent threads is described based on the notion of permission to access. Transfer of permission between threads subdivision and combination of permission is discussed. The roots of the approach are in Boyland s 3 demonstration of the utility of fractional permissions in specifying non-interference between concurrent threads. We add the notion of counting permission which mirrors the programming technique called permission counting. Both fractional and counting permissions permit passivity the specification that a program can be permitted to access a heap cell yet prevented from altering it. Models of both mechanisms are described. The use of two different mechanisms is defended. Some interesting problems are acknowledged and some intriguing possibilities for future development including the notion of resourcing as a step beyond typing are paraded. Categories and Subject Descriptors Software Program verification Correctness proofs Formal methods Validation Specifying and Verifying and Reasoning about Programs Logics of programs General Terms Languages theory verification Keywords separation logic concurrency permissions ACM 2005. This is the author s version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version will be published in proceedings of POPL 05 1-58113-830-X 05 0001 no ACM DOI available yet . 1. BACKGROUND Separation .

• Kế toán - Kiểm toán
• estate professionals
• keynote speaker
• Composite Natural Material
• Wood Polymer Composites
• Engineered Membranes
• Transporters