The Prpgress Propety In A Type System For Client-Server Interactions

With the development of Internet and communication technologies, parallel and distributed computing which supports distribution, concurrency, heterogeneity and interoperability has become an important research field in computer science. Structuring communication to ensure safe interaction of concurrent systems is a central issue in the theory and practice of parallel and distributed computing. Session type theory based on Pi-calculus provides a theoretical foundation of communication-centered programming, which is an effective formal method to structure interactions and reason over communicating processes and their behaviors. For the large amounts of programs which communicate by messages passing in parallel and distributed computing scenarios, session type theory can support the verification that the structure and sequence of messages are correct when receive or send messages. Type system based on the session type theory is a formal method which mainly focuses on how to categorize the values and expressions in programming languages into different types and express the interactions among these types. Type system can analyze programs and prevent the bad behaviors from occurring to ensure the safety of programming languages, which provides a safe, optimized, readable and modular function for programmers. Session type theory as well as type system derived are the focus of research in communication-centered distributed programming.This thesis mainly discusses the description of an indefinite number of repetitions of messages, progress property in both synchronous and asynchronous communications, as well as the local optimization of the sequence of messages in partially commutative asynchronous communications. The main contents and contributions of the thesis are as follows:(1) The current research work on session types and Pi-calculus is analyzed, and a bounded polymorphic type system with recursive session type is proposed. The definition of recursive session type in the present type system can be used to describe the behaviors with indefinite number of repetitions, making the server more flexible to provide not only one time service but also any number of times services. Moreover, the relaxed duality relation is defined combining the concept of subtype of session types, which relation not only makes the types on the two ports in a communication more flexible but also is helpful to the definition of type compliance and the research on the progress property later. Meanwhile, since the recursive session type itself is a kind of session type, the subtype and relaxed duality relation for recursive session type are defined in the present thesis.(2) Progress property is kept in synchronous and asynchronous communications, and the soundness and communication safety of type system are proved. The types of channels are distinguished between shared channels and live channels, and the cases that could lead to deadlocks are analyzed through specific examples in the two kinds of channels in different ways of communication. Further, the causes of deadlocks are explained and the ways to make the deadlocks free are presented. Based on the relaxed duality relation, type compliance and some other rules are defined, which rules make the type system keep progress property. In addition, subject reduction, type safety and progress theories are proved, indicating the soundness and communication safety of the present type system.(3) Especially, for partially commutative asynchronous binary sessions and multiparty sessions, the introduction of asynchronous communication subtyping makes it possible to permute and optimize the sequence of messages on each participant, which both improves the efficiency of communication and resolves the deadlocks in communications successfully. Moreover, the types of messages are distinguished between dependent and independent ones, and a series of action asynchronous subtyping rules are defined for the two kinds of types. However, the asynchronous communication subtyping will change the sequences and structures of messages. To ensure the safety of communication, the cases that could cause deadlocks are revealed, and the progress property is kept by the type system. In addition, to make such action permutations automatic, an algorithmic asynchronous subtyping is presented, associating the subtyping for session types with asynchronous communication subtyping.