Global progress for dynamically interleaved multiparty sessions

被引：75
作者：
Coppo, Mario [1 ]
Dezani-Ciancaglini, Mariangiola [1 ]
Yoshida, Nobuko [2 ]
Padovani, Luca [1 ]
机构：
[1] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy
[2] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London, England
来源：
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | 2016年 / 26卷 / 02期
基金：
英国工程与自然科学研究理事会;
关键词：
STRUCTURED COMMUNICATION; CALCULUS; SYSTEM;
D O I：
10.1017/S0960129514000188
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositional communication type system, a novel static interaction type system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.
引用
收藏
页码：238 / 302
页数：65
相关论文
共 63 条
[1]  
Acciai L, 2008, LECT NOTES COMPUT SC, V5065, P642, DOI 10.1007/978-3-540-68679-8_40
[2]  
[Anonymous], 2002, Types and Programming Languages
[3]  
Bettini L, 2008, LECT NOTES COMPUT SC, V5201, P418, DOI 10.1007/978-3-540-85361-9_33
[4]   Cryptographic Protocol Synthesis and Verification for Multiparty Sessions [J].
Bhargavan, Karthikeyan ;
Corin, Ricardo ;
Denielou, Pierre-Malo ;
Fournet, Cedric ;
Leifer, James J. .
PROCEEDINGS OF THE 22ND IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, 2009, :124-+
[5]  
Bocchi L, 2010, LECT NOTES COMPUT SC, V6269, P162, DOI 10.1007/978-3-642-15375-4_12
[6]  
Bocchi L, 2013, LECT NOTES COMPUT SC, V7892, P50
[7]  
Bonelli E, 2008, LECT NOTES COMPUT SC, V4912, P240
[8]  
Boreale M, 2008, LECT NOTES COMPUT SC, V5051, P19, DOI 10.1007/978-3-540-68863-1_3
[9]   ON COMMUNICATING FINITE-STATE MACHINES [J].
BRAND, D ;
ZAFIROPULO, P .
JOURNAL OF THE ACM, 1983, 30 (02) :323-342
[10]  
Bruni R, 2008, LECT NOTES COMPUT SC, V5140, P100
1234567