اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدAssuming Just Enough Fairness to make Session Types Complete for Lock-freedom
336
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
قيم البحث
اقرأ أيضاً
83 -
Bogdan Aman (Romanian Academy
, Institute of Computer Science andn A.I.Cuza University
, Iasi
2019
This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a typing system whi
ch extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its typing system are motivated and illustrated by a running example.
Session types are used to describe and structure interactions between independent processes in distributed systems. Higher-order types are needed in order to properly structure delegation of responsibility between processes. In this paper we show t
hat higher-order web-service contracts can be used to provide a fully-abstract model of recursive higher-order session types. The model is set-theoretic, in the sense that the meaning of a contract is given in terms of the set of contracts with which it complies. The proof of full-abstraction depends on a novel notion of the complement of a contract. This in turn gives rise to an alternative to the type duality commonly used in systems for type-checking session types. We believe that the notion of complement captures more faithfully the behavioural intuition underlying type duality.
We propose a version of chaotic inflation, in which a fundamental scale M, well below the Planck scale M_P, fixes the initial value of the effective potential. If this scale happens to be the scale of grand unified theories, there are just enough e-f
oldings of inflation. An initial epoch of fast-roll breaks scale-invariance at the largest observable scales.
Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, r
espectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow for simple and insightful characterizations of (at least some of) these combined inductive/coinductive properties of binary session types. In particular, we illustrate the role of corules in characterizing fair termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and fair subtyping, a liveness-preserving refinement relation for session types.
Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type
disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types, and an internal language with casts, for which operational semantics is given, and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
