Authors
Advisors
Abstract
Reasoning about concurrent programs is difficult due to the intricate interactions among agents. In general, concurrency can be classified into two categories: shared memory model and message-passing model. For shared memory model, in order for better performance and lower energy consumption, modern multi-core architectures allow out-of-order executions; and for different usage scenarios, different architectures may choose different relaxed models, e.g., X86-TSO, ARM, POWER, etc. The study of message-passing models also face many challenges: messages may be lost or duplicated during transition; and disjointed agents should consider various synchronization problems, for instance, deadlock, liveness, etc. Therefore, studying the semantics of concurrent systems is becoming more and more important.
On the other hand, due to wide application of concurrent systems, modern program verification require formal specification for inter-agent communication to achieve better modularity. The benefit that gained by modularity is to allow local reasoning of separated agents. The modification of one agent does not affect the implementation of others, as long as the modified one fits with several formal requirements.
Based on the above observation, this thesis presents a trace-based semantic framework for current programs. Concurrent operations in our framework produce abstract events which are linked up to form a Directed Acyclic Graph (DAG) describing an execution in an architecture-independent way. In order to support modularity, we define various operators and assertions to structurally specify trace structures. For relaxed memory models, the framework is flexible enough to simulate SC, TSO, and C11 models, and also can be extended to support various barriers and read-modify-write primitives. This framework is the first unified semantic system to provide formal specification for different relaxed memory models. For message-passing models, based on trace semantics, the thesis proposes two reasoning systems. One is for reliable message-passing systems, which allows local agents dynamically calculate their environmental expectations, and supports both temporal and spatial modularity. The other is for unreliable message-passing model, which uses temporal logic as the specification of agents' behaviors. Besides, using these reasoning systems, we prove two classical distributed algorithms: leader election algorithm and merge sort network.
Published
Chinese Version [PDF]