Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols

• Autorzy: Brad E. , Hammond K.
• Języki publikacji: EN

Abstrakty

EN

In the modern, multi-threaded, multi-core programming environment, correctly managing system resources, including locks and shared variables, can be especially difficult and errorprone. A simple mistake, such as forgetting to release a lock, can have major consequences on the correct operation of a program, by, for example, inducing deadlock, often at a time and location that is isolated from the original error. In this paper, we propose a new type-based approach to resource management, based on the use of dependent types to construct a Domain-Specific Embedded Language (DSEL) whose typing rules directly enforce the formal program properties that we require. In this way, we ensure strong static guarantees of correctness-by-construction, without requiring the development of a new special-purpose type system or the associated special-purpose soundness proofs. We also reduce the need for "over-serialisation", the overly-conservative use of locks that often occurs in manually constructed software, where formal guarantees cannot be exploited. We illustrate our approach by implementing a DSEL for concurrent programming and demonstrate its applicability with reference to an example based on simple bank account transactions.

Słowa kluczowe

EN

concurrent programming; domain specific language (DSL)

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 2
• Strony: 145--176
• Opis fizyczny: Bibliogr. 48 poz.

Twórcy

autor

Brad E.

autor

Hammond K.

• School of Computer Science, University of St Andrews, Jack Cole Building, North Haugh, St Andrews, Fife KY16 9SX, United Kingdom,

Bibliografia

• [1] Agha, G., Mason, I., Smith, S., Talcott, C.: A foundation for actor computation, Journal of Functional Programming, 7(1), 1997, 1-72.
• [2] Amey, P.: Correctness by construction: better can also be cheaper, CrossTalk: The Journal of Defense Software Engineering, 15(3), 2002, 24-28.
• [3] Bhatti, S., Brady, E., Hammond, K., McKinna, J.: Domain specific languages (DSLs) for network protocols (position paper), Proc. of Workshops of 29th IEEE Int. Conf. on Distributed Computing Systems, ICDCS 2009 (Montreal, June 2009), IEEE Computer Society Press, 2009, 208-213.
• [4] Brady, E.: Practical Implementation of a Dependently Typed Functional Programming Language, PhD thesis, University of Durham, 2005.
• [5] Brady, E.: Ivor, a proof engine, Revised Selected Papers from 18th Int. Workshop on Implementation and Application of Functional Languages, IFL 2006 (Budapest, Sept. 2006) (Z. Horv´ath, V. Zs´ok, A. Butterfield, Eds.), Lect. Notes in Comput. Sci., 4449, Springer-Verlag, 2007, 145-162.
• [6] Brady, E., Hammond, K.: A dependently typed framework for static analysis of program execution costs, Revised Selected Papers from 17th Int. Workshop on Implementation and Application of Functional Languages, IFL 2005 (Dublin, Sept. 2005) (A. Butterfield, C. Grelck, F. Huch, Eds.), Lect. Notes in Comput. Sci., 4015, Springer-Verlag, 2006, 74-90.
• [7] Brady, E., Hammond, K.: A verified staged interpreter is a verified compiler, Proc. of 5th Int. Conf. On Generative Programming and Component Engineering, GPCE '06 (Portland, OR, Oct. 2006), ACM Press, 2006, 111-120.
• [8] Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices, Revised Selected Papers from Int. Workshop on Types for Proofs and Programs, TYPES 2003 (Torino, Apr.-May 2003) (S. Berardi, M. Coppo, F. Damiani, Eds.), Lect. Notes in Comput. Sci., 3085, Springer-Verlag, 2004, 115-129.
• [9] Butenhof, D. R.: Programming with POSIX Threads, Addison Wesley, 1997.
• [10] Coffman, E., Elphick, M., Shoshani, A.: System deadlocks, ACM Computing Surveys, 3(2), 1971, 67-78.
• [11] Czarnecki, K., O'Donnell, J., Striegnitz, J., Taha,W.: DSL implementation in MetaOCaml, Template Haskell, and C++, Revised Papers from Int. Seminar on Domain Specific Program Generation (Dagstuhl Castle, March 2003) (C. Lengauer, D. S. Batory, C. Consel, M. Odersky, Eds.), Lect. Notes in Comput. Sci., 3016, Springer-Verlag, 2004, 51-72.
• [12] Elliott, C., Hudak, P.: Functional reactive animation, Proc. of 2nd ACM SIGPLAN Int. Conf. on Functional Programming, ICFP '97 (Amsterdam, June 1997), ACM Press, 1997, 263-273.
• [13] Ennals, R.: Software Transactional Memory Should Not Be Abstraction Free, Technical report IRC-TR-06-052, Intel Research, 2006.
• [14] Goguen, H.: A Typed Operational Semantics for Type Theory, PhD Thesis, University of Edinburgh, 1994.
• [15] Hammond, K., Michaelson, G.: Hume: a domain-specific language for real-time embedded systems, Proc. Of 2nd Int. Conf. on Generative Programming and Component Engineering, GPCE '03 (F. Pfenning, Y. Smaragdakis, Eds.), Lect. Notes in Comput. Sci., 2830, Springer-Verlag, 2003, 37-56.
• [16] Hancock, P., Setzer, A.: Interactive programs in dependent type theory, Proc. of 14th Annual Conf. of EACSL, CSL 2000 (Fischbachau, Aug. 2000) (P. Clote, H. Schwichtenberg, Eds.), Lect. Notes in Comput. Sci., 1862, Springer-Verlag, 2000, 317-331.
• [17] Harris, T., Marlow, S., Peyton Jones, S., Herlihy, M.: Composable memory transactions, Proc. of 10th ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming, PPoPP 2005 (Chicago, IL, June 2005), ACM Press, 2005, 48-60.
• [18] Hawblitzel, C.: Linear Types for Aliased Resources, Technical report MSR-TR-2005-141, Microsoft Research, 2005.
• [19] Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs, Conf. Record of 30th SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2003 (New Orleans, LA, Jan. 2003), ACM Press, 2003, 185-197.
• [20] Hudak, P.: Building domain-specific embedded languages, ACM Computing Surveys, 28(4es), 1996, 196.
• [21] Igarashi, A., Kobayashi, N.: Type-based analysis of communication for concurrent programming languages, Proc. of 4th Int. Symposium on Static Analysis, SAS '97 (Paris, Sept. 1997) (P. Van Hentenryck, Ed.), Lect. Notes in Comput. Sci., 1302, Springer-Verlag, 1997, 187-201.
• [22] Igarashi, A., Kobayashi, N.: Resource usage analysis, Conf. Record of 29th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2002 (Portland, OR, Jan. 2002), ACM Press, 2002, 331-342.
• [23] Jin, N., He, J.: Towards a truly concurrent model for processes sharing resources, Proc. of 3rd IEEE Int. Conf. on Software Engingeering and Formal Methods, SEFM '05 (Koblenz, Sept. 2005), IEEE Computer Society Press, 2005, 231-239.
• [24] Kiselyov, O., Shan, C.-C.: Lightweight static resources: Sexy types for embedded and systems programming, Draft Proc. of 8th Symp. on Trends in Functional Programming, TFP '07 (New York, Apr. 2007), 2007.
• [25] Kobayashi, N.: A type system for lock-free processes, Information and Computation, 177(2), 2002, 122-159.
• [26] Kobayashi, N., Pierce, B. C., Turner, D. N.: Linearity and the pi-calculus, ACM Transactions on Programmming Languages and Systems, 21(5), 1999, 914-947.
• [27] Landin, P.: The next 700 programming languages, Communications of the ACM, 9(3), 1966, 157-166.
• [28] Leijen, D.: Parsec, a fast combinator parser, http://www.cs.uu.nl/~daan/parsec.html, 2001.
• [29] Ligatti, J. A.: Policy Enforcement via Program Monitoring, PhD thesis, 2006.
• [30] Löh, A., McBride, C., Swierstra, W.: A tutorial implementation of a dependently typed lambda calculus, in this issue.
• [31] Marathe, V. J., Moir, M.: Efficient nonblocking software transactional memory, Proc. of 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '07 (San Jose, CA, March 2007), ACM Press, 2007, 136-137.
• [32] Marriott, K., Stuckey, P., Sulzmann, M.: Resource usage verification, Proc. of 1st Asian Symposium on Programming Languages and Systems, APLAS 2003 (Beijing, Nov. 2003) (A. Ohori, Ed.), Lect. Notes in Comput. Sci., 2895, Springer-Verlag, 2003, 212-229.
• [33] McBride, C.: Epigram: Practical programming with dependent types, Revised Lectures from 5th Int. School on Advanced Functional Programming, AFP 2004 (Tartu, Aug. 2004) (V. Vene, T. Uustalu, Eds.), Lect. Notes in Comput. Sci., 3622, Springer-Verlag, 2005, 130-170.
• [34] McBride, C., McKinna, J.: The view from the left, Journal of Functional Programming, 14(1), 2004, 69-111.
• [35] Nanevski, A., Govereau, P., Morrisett, G.: Towards type-theoretic semantics for transactional concurrency, Proc. of 2009 ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI '09 (Savannah, Jan. 2009), ACM Press, 2009, 79-90.
• [36] Nanevski, A., Morisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory, Proc. of 11th ACM SIGPLAN 2006 Int. Conf. on Functional Programming, ICFP 2006 (Portland, OR, Sept. 2006), ACM Press, 2006, 62-73.
• [37] Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs, Proc. of 13th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2008 (Victoria, BC, Sept. 2008), ACM Press, 2008, 229-240.
• [38] Oaks, S., Wong, H.: Java Threads, 3rd ed. O'Reilly, 2004.
• [39] Pašalıc, E., Taha,W., Sheard, T.: Tagless staged interpreters for typed languages, Proc. of 7th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2002 (Pittburgh, PA, Oct. 2002), ACM Press, 2002, 218-229.
• [40] Peyton Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs, Proc. of 11th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2006 (Portland, OR, Sept. 2006), ACM Press, 2006, 50-61.
• [41] Peyton Jones, S. L., Wadler, P.: Imperative functional programming, Conf. Record of 20th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL '93 (Charleston, SC, Jan. 1993), ACM Press, 1993, 71-84.
• [42] Popeea, C., Chin, W.-N.: A type system for resource protocol verification and its correctness proof, Proc. of 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM '04 (Verona, Aug. 2004), ACM Press, 2004, 135-146.
• [43] Sheard, T.: Languages of the future, Companion to 19th Annual ACM SIGPLAN Conf. on Object Oriented Programming Systems, Languages and Applications, OOPSLA '04 (Vancouver, BC, Oct. 2004), ACM Press, 2004, 116-119.
• [44] Suenaga, K., Kobayashi, N.: Type-based analysis of deadlock for a concurrent calculus with interrupts, Proc. of 16th European Symposium on Programming, ESOP 2007 (Braga, March 2007) (R. de Nicola, Ed.), Lect. Notes in Comput. Sci., 4421, Springer-Verlag, 2007, 490-504.
• [45] Sutter, H.: Use lock hierarchies to avoid deadlock, Dr Dobb's Journal, 33(1), 2008.
• [46] Taha, W.: Multi-Stage Programming: Its Theory and Applications, PhD thesis, Oregon Graduate Inst. Of Science and Technology, 1999.
• [47] Turner, D. A.: Elementary strong functional programming, Proc. of 1st Int. Symposium on Functional Programming Languages in Education, FLPE '95 (Nijmegen, Dec. 1995) (P. Hartel, R. Plasmeijer, Eds.), Lect. Notes in Comput. Sci., 1022, Springer-Verlag, 1995, 1-13.
• [48] Walker, D.: A Type system for expressive security policies, Proc. of 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000 (Boston, MA, Jan. 2000), ACM Press, 2000, 254-267.