Advertisement

Resource Protection Using Atomics

Patterns and Verification
  • Afshin Amighi
  • Stefan Blom
  • Marieke Huisman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)

Abstract

For the verification of concurrent programs, it is essential to be able to show that synchronisation mechanisms are implemented correctly. A common way to implement such sychronisers is by using atomic operations. This paper identifies what different synchronisation patterns can be implemented by using atomic read, write and compare-and-set operation. Additionally, this paper proposes also a specification of these operations in Java’s AtomicInteger class, and shows how different synchronisation mechanisms can be built and verified using atomic integer as the synchronisation primitive.

The specifications for the methods in the AtomicInteger class are derived from the classical concurrent separation logic rule for atomic operations. A main characteristic of our specification is its ease of use. To verify an implementation of a synchronisation mechanism, the user only has to specify (1) what are the different roles of the threads participating in the synchronisation, (2) what are the legal state transitions in the synchroniser, and (3) what share of the resource invariant can be obtained in a certain state, given the role of the current thread. The approach is illustrated on several synchronisation mechanisms. For all implementations, we provide a machine-checked proof that the implementations correctly implement the synchroniser.

Keywords

Shared Resource Resource Protection Synchronisation Mechanism Atomic Location Separation Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Amighi, A., Blom, S.C.C., Huisman, M.: Resource protection using atomics: patterns and verifications. Technical Report TR-CTIT-13-10, Centre for Telematics and Information Technology, University of Twente, Enschede (May 2013)Google Scholar
  2. 2.
    Amighi, A., Blom, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Formal specifications for Java’s synchronisation classes. In: Lafuente, A.L., Tuosto, E. (eds.) 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pp. 725–733. IEEE Computer Society (2014)Google Scholar
  3. 3.
    Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259–270. ACM (2005)Google Scholar
  4. 4.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212–232 (2005)CrossRefGoogle Scholar
  6. 6.
    Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 259–270. ACM, New York (2011)Google Scholar
  8. 8.
    Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for multithreaded Java programs (submitted, 2014)Google Scholar
  10. 10.
    Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT, POPL 2011, pp. 271–282. ACM, New York (2011)Google Scholar
  12. 12.
    Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 247–255. IEEE (2010)Google Scholar
  13. 13.
    Leino, K., 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)Google Scholar
  14. 14.
    Ley-Wild, R., Nanevski, A.: Subjective auxiliary state for coarse-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 561–574. ACM (2013)Google Scholar
  15. 15.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Parkinson, M.J.: Local reasoning for Java. Tech. Rep. UCAM-CL-TR-654, University of Cambridge, Computer Laboratory (November 2005)Google Scholar
  17. 17.
    Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Principles of Programming Languages (POPL 2008), pp. 75–86. ACM Press (2008)Google Scholar
  18. 18.
    Raynal, M.: Concurrent Programming - Algorithms, Principles, and Foundations. Springer (2013)Google Scholar
  19. 19.
    Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002)Google Scholar
  20. 20.
    Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014)Google Scholar
  21. 21.
    Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169–188. Springer, Heidelberg (2013)Google Scholar
  22. 22.
    Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Vafeiadis, V.: Concurrent separation logic and operational semantics. Electr. Notes Theor. Comput. Sci. 276, 335–351 (2011)MathSciNetCrossRefGoogle Scholar
  24. 24.
  25. 25.

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Afshin Amighi
    • 1
  • Stefan Blom
    • 1
  • Marieke Huisman
    • 1
  1. 1.Formal Methods and ToolsUniversity of TwenteEnschedeThe Netherlands

Personalised recommendations