Abstract
The capability calculus is a framework for statically reasoning about program resources such as deallocatable memory regions. Fractional capabilities, originally proposed by Boyland for checking the determinism of parallel reads in multi-thread programs, extend the capability calculus by extending the capabilities to range over the rational numbers. Fractional capabilities have since found numerous applications, including race detection, buffer bound inference, security analyses, and separation logic. However, previous work on fractional capability systems either lacked polymorphism or lacked an efficient inference procedure. Automated inference is important for the application of the calculus to static analysis. This paper addresses the issue by presenting a polymorphic fractional capability calculus that allows polynomial-time inference via a reduction to rational linear programming.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
GNU Linear Programming Kit, http://www.gnu.org/software/glpk/glpk.html
Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, pp. 301–320 (2007)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 259–270 (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Crary, K., Walker, D., Morrisett, G.: Typed memory management in a calculus of capabilities. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 262–275 (1999)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 1–12 (2002)
Kikuchi, D., Kobayashi, N.: Type-based verification of correspondence assertions for communication protocols. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 191–205. Springer, Heidelberg (2007)
Pratikakis, P., Foster, J.S., Hicks, M.: Locksmith: context-sensitive correlation analysis for race detection. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 320–331 (2006)
Rehof, J., Fähndrich, M.: Type-base flow analysis: from polymorphic subtyping to cfl-reachability. In: Proceedings of the 23th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 54–66 (2001)
Terauchi, T.: Checking race freedom via linear programming. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, pp. 1–10 (2008)
Terauchi, T.: A type system for observational determinism. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF, pp. 287–300 (2008)
Terauchi, T., Aiken, A.: Witnessing side-effects. In: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP, pp. 105–115 (2005)
Terauchi, T., Aiken, A.: A capability calculus for concurrency and determinism. ACM Trans. Program. Lang. Syst. (2008)
Terauchi, T., Megacz, A.: Inferring channel buffer bounds via linear programming. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 284–298. Springer, Heidelberg (2008)
Tofte, M., Talpin, J.P.: Implementation of the typed call-by-value λ-calculus using a stack of regions. In: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 188–201 (1994)
Yasuoka, H., Terauchi, T.: Polymorphic fractional capabilities(long version) (2008), http://www.kb.ecei.tohoku.ac.jp/~yasuoka/papers/polyfrac.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yasuoka, H., Terauchi, T. (2009). Polymorphic Fractional Capabilities. In: Palsberg, J., Su, Z. (eds) Static Analysis. SAS 2009. Lecture Notes in Computer Science, vol 5673. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03237-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-03237-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03236-3
Online ISBN: 978-3-642-03237-0
eBook Packages: Computer ScienceComputer Science (R0)