A Type Theory for Robust Failure Handling in Distributed Systems

详细信息    查看全文

• 关键词：Session types ; Partial failure handling ; Distributed systems
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9688
• 期：1
• 页码：96-113
• 全文大小：710 KB
• 参考文献：1.Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)CrossRef
  2.Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 285–300. Springer, Heidelberg (2009)CrossRef
  3.Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. MSCS 29, 1–50 (2015)MATH
  4.Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402–417. Springer, Heidelberg (2008)CrossRef
  5.Carbone, M., Yoshida, N., Honda, K.: Asynchronous session types: exceptions and multiparty interactions. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 187–212. Springer, Heidelberg (2009)CrossRef
  6.Collet, R., Van Roy, P.: Failure handling in a network-transparent distributed programming language. In: Cheraghchi, H.S., Lindskov Knudsen, J., Romanovsky, A., Babu, C.S. (eds.) Exception Handling. LNCS, vol. 4119, pp. 121–140. Springer, Heidelberg (2006)CrossRef
  7.Colombo, C., Pace, G.J.: Recovery within long-running transactions. ACM Comput. Surv. 45(3), 28: 1–28: 35 (2013)CrossRef MATH
  8.Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011, pp. 435–446 (2011)
  9.Technical report. Long version of this paper. https://​github.​com/​Distributed-Systems-Programming-Group/​paper/​blob/​master/​2016/​forte16_​long_​dsp.​pdf
  10.Gärtner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1–26 (1999)CrossRef
  11.Guidi, C., Lanese, I., Montesi, F., Zavattaro, G.: On the interplay between fault handling and request-response service invocations. In: 8th International Conference on Application of Concurrency to System Design, 2008, ACSD 2008, pp. 190–198, June 2008
  12.Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273–284. ACM (2008)
  13.Hu, R., Neykova, R., Yoshida, N., Demangeon, R., Honda, K.: Practical interruptible conversations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 130–148. Springer, Heidelberg (2013)CrossRef
  14.Jakšić, S., Padovani, L.: Exception handling for copyless messaging. Sci. Comput. Program. 84, 22–51 (2014)CrossRef MATH
  15.Lanese, I., Montesi, F.: Error handling: from theory to practice. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 66–81. Springer, Heidelberg (2010)CrossRef
  16.Lanese, I., Montesi, F., Zavattaro, G.: Amending choreographies. In: WWV 2013, vol. 123 of EPTCS, pp. 34–48 (2013)
  17.Mostrous, D.: Session Types, in Concurrent Calculi: Higher-Order Processes and Objects. Ph.D. thesis, Imperial College London (2009)
  18.Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH
  19.Takeuchi, K., Honda, H., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, Constantinos, Philokyprou, G., Maritsas, D., Theodoridis, Sergios (eds.) PARLE 1994. LNCS, vol. 817. Springer, Heidelberg (1994)
  20.Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: a model of service-oriented computation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 269–283. Springer, Heidelberg (2008)CrossRef
  21.Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 171(4), 73–93 (2007)CrossRef
  
• 作者单位：Tzu-Chun Chen (15)
  Malte Viering (15)
  Andi Bejleri (15)
  Lukasz Ziarek (16)
  Patrick Eugster (15) (17)
  
  15. Department of Computer Science, TU Darmstadt, Darmstadt, Germany
  16. Department of Computer Science and Engineering, SUNY Buffalo, New York, USA
  17. Department of Computer Science, Purdue University, West Lafayette, USA
  
• 丛书名：Formal Techniques for Distributed Objects, Components, and Systems
• ISBN：978-3-319-39570-8
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9688

文摘

This paper presents a formal framework for programming distributed applications capable of handling partial failures, motivated by the non-trivial interplay between failure handling and messaging in asynchronous distributed environments. Multiple failures can affect protocols at the level of individual interactions (alignment). At the same time, only participants affected by a failure or involved in its handling should be informed of it, and its handling should not be mixed with that of other failures (precision). This is particularly challenging, as through the structure of protocols, failures may be linked to others in subsequent or concomitant interactions (causality). Last but not least, no central authority should be required for handling failures (decentralisation). Our goal is to give developers a description language, called protocol types, to specify robust failure handling that accounts for alignment, precision, causality, and decentralisation. A type discipline is built to statically ensure that asynchronous failure handling among multiple endpoints is free from orphan messages, deadlocks, starvation, and interactions are never stuck.