- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Inferring and asserting distributed invariants
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Inferring and asserting distributed invariants Grant, Stewart
Abstract
Distributed systems are difficult to debug and understand. A key reason for this is distributed state, which is not easily accessible and must be pieced together from the states of the individual nodes in the system. We propose Dinv, an automatic approach to help developers of distributed sys- tems uncover the runtime distributed state properties of their systems. Dinv uses static and dynamic program analyses to infer relations between variables at differ- ent nodes. For example, in a leader election algorithm, Dinv can relate the variable leader at different nodes to derive the invariant ∀ nodes i, j, leader i = leader j . This can increase the developer’s confidence in the correctness of their system. The developer can also use Dinv to convert an inferred invariant into a distributed runtime assertion on distributed state. We applied Dinv to several popular distributed systems, such as etcd Raft, Hashicorp Serf, and Taipei-Torrent, which have between 1.7K and 144K LOC and are widely used. Dinv derived useful invariants for these systems, including invari- ants that capture the correctness of distributed routing strategies, leadership, and key hash distribution. We also used Dinv to assert correctness of the inferred etcd Raft invariants at runtime, using these asserts to detect injected silent bugs.
Item Metadata
Title |
Inferring and asserting distributed invariants
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2018
|
Description |
Distributed systems are difficult to debug and understand. A key reason for this is
distributed state, which is not easily accessible and must be pieced together from
the states of the individual nodes in the system.
We propose Dinv, an automatic approach to help developers of distributed sys-
tems uncover the runtime distributed state properties of their systems. Dinv uses
static and dynamic program analyses to infer relations between variables at differ-
ent nodes. For example, in a leader election algorithm, Dinv can relate the variable
leader at different nodes to derive the invariant ∀ nodes i, j, leader i = leader j .
This can increase the developer’s confidence in the correctness of their system.
The developer can also use Dinv to convert an inferred invariant into a distributed
runtime assertion on distributed state.
We applied Dinv to several popular distributed systems, such as etcd Raft,
Hashicorp Serf, and Taipei-Torrent, which have between 1.7K and 144K LOC and
are widely used. Dinv derived useful invariants for these systems, including invari-
ants that capture the correctness of distributed routing strategies, leadership, and
key hash distribution. We also used Dinv to assert correctness of the inferred etcd
Raft invariants at runtime, using these asserts to detect injected silent bugs.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2018-08-27
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NoDerivatives 4.0 International
|
DOI |
10.14288/1.0371258
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2018-09
|
Campus | |
Scholarly Level |
Graduate
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NoDerivatives 4.0 International