Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2008: Programming Languages and Systems pp 155–170Cite as

Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5356))

Abstract

We present a type-based deadlock-freedom verification for concurrent programs with non-block-structured lock primitives and mutable references. Though those two features are frequently used, they are not dealt with in a sufficient manner by previous verification methods. Our type system uses a novel combination of lock levels, obligations and ownerships. Lock levels are used to guarantee that locks are acquired in a specific order. Obligations and ownerships guarantee that an acquired lock is released exactly once.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Flanagan, C., Freund, S.N.: Types for safe locking: Static race detection for Java. ACM Transactions on Programming Languages and Systems 28(2), 207–255 (2006)

    Article  Google Scholar 

  2. Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2002), SIGPLAN Notices, November 2002. vol. 37, pp. 211–230 (2002)

    Google Scholar 

  3. Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack size analysis for interrupt-driven programs. Information and Computation 194(2), 144–174 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dahyabhai, N.: Bugzilla Bug 439215: dbus-daemon-1 hangs when using the option nss_initgroups_ignoreusers in /etc/ldap.conf. with the user root. Red Hat, Inc (accessed on June 19, 2008) (March 2008), https://bugzilla.redhat.com/show_bug.cgi?id=439215

  6. Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Programming Language Design and Implementation (PLDI) (June 2008)

    Google Scholar 

  7. Flanagan, C., Abadi, M.: Object types against races. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 288–303. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Flanagan, C., Abadi, M.: Types for safe locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 91–108. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1–12 (2002)

    Google Scholar 

  10. Kikuchi, D., Kobayashi, N.: Type-based verification of correspondence assertions for communication protocols. In: Proceedings of the Fifth ASIAN Symposium on Programming Languages and Systems (November 2007)

    Google Scholar 

  11. Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  12. Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Kobayashi, N.: Substructural type systems for program analysis. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, p. 14. Springer, Heidelberg (2008), http://www.kb.ecei.tohoku.ac.jp/~koba/slides/FLOPS2008.pdf

    Chapter  Google Scholar 

  14. Kobayashi, N., Saito, S., Sumii, E.: An implicitly-typed deadlock-free process calculus. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 489–503. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Palsberg, J., Ma, D.: A typed interrupt calculus. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 291–310. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Suenaga, K., Kobayashi, N.: Type-based analysis of deadlock for a concurrent calculus with interrupts. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 490–504. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  17. Terauchi, T.: Types for Deterministic Concurrency. PhD thesis, Electrical Engineering and Computer Sciences, University of California at Berkeley (August 2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tohoku University, Japan

    Kohei Suenaga

Authors
  1. Kohei Suenaga
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research India, 196/36, 2nd Main, Sadashivnagar, 560080, Bangalore, India

    G. Ramalingam

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Suenaga, K. (2008). Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89330-1_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89329-5

  • Online ISBN: 978-3-540-89330-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation