Abstract
In the multicore era, verification for concurrent programs is increasingly important. Although state-of-the-art verification systems ensure safe concurrent accesses to heap data structures, they tend to ignore program variables. This is problematic since these variables might also be accessed by concurrent threads. One solution is to apply the same permission system, designed for heap memory, to variables. However, variables have different properties than heap memory and could benefit from a simpler reasoning scheme. In this paper, we propose a new permission system to ensure safe accesses to shared variables. Given a shared variable, a thread owns either a full permission or no permission at all. This ensures data-race freedom when accessing variables. Our goal is to soundly manage the transfer of variable permissions among threads. Moreover, we present an algorithm to automatically infer variable permissions from procedure specifications. Though we propose a simpler permission scheme, we show that our scheme is sufficiently expressive to capture programming models such as POSIX threads and Cilk. We also implement this new scheme inside a tool, called Vperm, to automatically verify the correctness of concurrent programs based on given pre/post-specifications.
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
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.: Permission Accounting in Separation Logic. In: ACM Symposium on Principles of Programming Languages, pp. 259–270. ACM, New York (2005)
Bornat, R., Calcagno, C., Yang, H.: Variables as Resource in Separation Logic. Electronic Notes in Theoretical Computer Science 155, 247–276 (2006)
Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Butenhof, D.R.: Programming with POSIX Threads. Addison-Wesley Longman Publishing Co., Inc., Boston (1997)
Demaine, E.D.: C to Java: Converting Pointers into References. Concurrency - Practice and Experience 10(11-13), 851–861 (1998)
Ferrara, P., Müller, P.: Automatic Inference of Access Permissions. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 202–218. Springer, Heidelberg (2012)
Frigo, M., Leiserson, C.E., Randall, K.H.: The Implementation of the Cilk-5 Multithreaded Language. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation, New York, NY, USA, pp. 212–223 (1998)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)
Heule, S., Leino, K.R.M., Müller, P., Summers, A.J.: Fractional Permissions Without the Fractions. In: Proceedings of the International Workshop on Formal Techniques for Java-like Programs (July 2011)
Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)
Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: ACM Symposium on Principles of Programming Languages, New York, NY, USA, pp. 271–282 (2011)
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)
Laffra, C.: A C++ to Java Translator. In: Advanced Java: Idioms, Pitfalls, Styles and Programming Tips, ch. 4. Prentice Hall Computer Books (1996)
Le, D.K., Chin, W.N., Teo, Y.M.: Variable Permissions for Concurrency Verification. Technical report, National University of Singapore (April 2012)
Leino, K.R.M., Müller, P.: A Basis for Verifying Multi-threaded Programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009)
Leino, K.R.M., Müller, P., Smans, J.: Verification of Concurrent Programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007/2008/2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009)
Mattson, T., Sanders, B., Massingill, B.: Patterns for Parallel Programming, 1st edn. Addison-Wesley Professional (2004)
Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated Verification of Shape and Size Properties Via Separation Logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)
O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)
Owicki, S., Gries, D.: Verifying Properties of Parallel Programs: an Axiomatic Approach. Communications of the ACM, 279–285 (1976)
Parkinson, M., Bornat, R., Calcagno, C.: Variables as Resource in Hoare Logics. In: IEEE Logic in Computer Science, Washington, DC, USA, pp. 137–146 (2006)
Reddy, U.S., Reynolds, J.C.: Syntactic Control of Interference for Separation Logic. In: ACM Symposium on Principles of Programming Languages, New York, NY, USA, pp. 323–336 (2012)
Reynolds, J.: Separation Logic: A Logic for Shared Mutable Data Structures. In: IEEE Logic in Computer Science, Copenhagen, Denmark (July 2002)
Tuerk, T.: A Separation Logic Framework for HOL. PhD thesis. University of Cambridge (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Le, DK., Chin, WN., Teo, YM. (2012). Variable Permissions for Concurrency Verification. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-34281-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34280-6
Online ISBN: 978-3-642-34281-3
eBook Packages: Computer ScienceComputer Science (R0)