Skip to main content
SpringerLink
Log in

A Type System for Counting Logs of Multi-threaded Nested Transactional Programs

  • Conference paper
  • First Online:
Distributed Computing and Internet Technology (ICDCIT 2016)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 9581))

Abstract

We present a type system to estimate an upper bound for the resource consumption of nested and multi-threaded transactional programs. The resource is abstracted as transaction logs. In comparison to our previous work on type and effect systems for Transactional Featherweight Java, this work exploits the natural composition of thread creation to give types to sub-terms. As a result, our new type system is simpler and more effective than our previous one. More important, it is more precise than our previous type system. We also show a type inference algorithm that we have implemented in a prototype tool.

This research is funded by Vietnam National Foundation for Science and Technology Development (NAFOSTED) under grant number 102.03-2014.23. The research is also partly supported by the research project QG.14.06, Vietnam National University, Hanoi.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

Notes

  1. 1.

    We can avoid the insertion as shown in our implementation for the type inference algorithm in Sect. 6.

  2. 2.

    https://github.com/truonganhhoang/tfj-infer.

References

  1. Bezem, M., Hovland, D., Truong, H.: A type system for counting instances of software components. Theor. Comput. Sci. 458, 29–48 (2012)

    Article  MATH  Google Scholar 

  2. Braberman, V., Garbervetsky, D., Yovine, S.: A static analysis for synthesizing parametric specifications of dynamic memory consumption. J. Object Technol. 5(5), 31–58 (2006)

    Article  Google Scholar 

  3. Chin, W.-N., Nguyen, H.H., Qin, S.C., Rinard, M.: Memory usage verification for OO programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 70–86. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proceedings of POPL 2003. ACM, January 2003

    Google Scholar 

  5. Hofmann, M.O., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  6. Jagannathan, S., Vitek, J., Welc, A., Hosking, A.: A transactional object calculus. Sci. Comput. Program. 57(2), 164–186 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  7. Mai Thuong Tran, T., Steffen, M., Truong, H.: Compositional static analysis for implicit join synchronization in a transactional setting. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 212–228. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Pham, T.-H., Truong, A.-H., Truong, N.-T., Chin, W.-N.: A fast algorithm to compute heap memory bounds of Java Card applets. In: Software Engineering and Formal Methods (2008)

    Google Scholar 

  9. Shavit, N., Touitou, D.: Software transactional memory. In: Symposium on Principles of Distributed Computing, pp. 204–213 (1995)

    Google Scholar 

  10. Vu, X.-T., Mai Thuong Tran, T., Truong, A.-H., Steffen, M.: A type system for finding upper resource bounds of multi-threaded programs with nested transactions. In: Symposium on Information and Communication Technology SoICT 2012, pp. 21–30 (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. VNU University of Engineering and Technology, Hanoi, Vietnam

    Anh-Hoang Truong, Dang Van Hung & Duc-Hanh Dang

  2. Japan Advanced Institute of Science and Technology, Nomi, Japan

    Xuan-Tung Vu

Authors
  1. Anh-Hoang Truong
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dang Van Hung
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Duc-Hanh Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xuan-Tung Vu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anh-Hoang Truong .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Nikolaj Bjørner

  2. Indian Institute of Technology Delhi, New Delhi, India

    Sanjiva Prasad

  3. IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA

    Laxmi Parida

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Truong, AH., Van Hung, D., Dang, DH., Vu, XT. (2016). A Type System for Counting Logs of Multi-threaded Nested Transactional Programs. In: Bjørner, N., Prasad, S., Parida, L. (eds) Distributed Computing and Internet Technology. ICDCIT 2016. Lecture Notes in Computer Science(), vol 9581. Springer, Cham. https://doi.org/10.1007/978-3-319-28034-9_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-28034-9_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-28033-2

  • Online ISBN: 978-3-319-28034-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation