Trade-offs in distributed concurrency control

For more info about our services contact : help@bestpfe.com

Table of contents

List of Tables
List of Figures
1 Introduction
1.1 Contributions
1.1.1 Proving invariant safety for highly-available distributed applications
1.1.2 A safe, convergent and highly-available replicated tree
1.1.3 Trade-offs in distributed concurrency control
I Verifying the design of distributed applications
Introduction to Part I
2 Proving invariant safety for highly-available distributed applications
2.1 System Model
2.1.1 General Principles
2.1.2 Notations and Assumptions
2.1.3 Operational Semantics
2.1.4 Operational Semantics with State History
2.1.5 Correspondence between the semantics
2.2 Proving convergence: Strong Eventual Consistency
2.2.1 Semilattice of auction object
2.3 Proving Invariants
2.3.1 Invariance Conditions
2.3.2 Applying the proof rule
2.3.3 Coordination for Invariant Preservation
3 Use cases
3.1 Distributed Barrier
3.2 Replicated lock
3.3 Courseware
3.3.1 Pseudocode of courseware
4 Automation
4.1 Specifying a distributed application in Soteria
4.2 Verification passes
4.2.1 Syntax check
4.2.2 Convergence check
4.2.3 Safety check
4.3 Tool evaluation
5 Related work
6 Conclusion of Part I and Future work
6.1 Future work
II Designing conflict resolution policies
Introduction to Part II
7 Design of a safe, convergent and coordination free replicated tree
7.1 System Model
7.2 Properties and associated proof rules
7.2.1 Sequential safety
7.2.2 Concurrency
7.2.2.1 Convergence
7.2.2.2 Precondition stability
7.2.2.3 Independence
7.2.3 Mechanized verification
7.3 Sequential specification of a tree
7.3.1 State
7.3.2 Invariant
7.3.3 Operations
7.3.4 Mechanized verification of the sequential specification
7.4 Concurrent tree specification
7.4.1 Precondition stability
7.4.1.1 Stability of add operation
7.4.1.2 Stability of remove operation
7.4.1.3 Stability of move operation
7.5 Safety of concurrent moves
7.5.1 Classifying moves
7.5.2 Coordination-free conflict resolution for concurrent moves
7.6 Convergence
7.7 Independence
7.7.1 Independence of add operation
7.7.2 Independence of remove operation
7.7.3 Independence of up-move operation
7.7.4 Independence of down-move operation
7.8 Safe specification of a replicated tree
7.8.1 Mechanized verification of the concurrent specification
7.9 Discussion
7.9.1 Moving from causal consistency to eventual consistency
7.9.2 Message overhead for conflict resolution
7.9.3 Computing the set of concurrent moves
8 Experimental study and Comparison
9 Related work
10 Conclusion of Part II and Future work
10.1 Future work
III Selecting Distributed Concurrency Control
Introduction to Part III
11 Exploring the coordination lattice
11.1 System Model
11.1.1 Application model
11.1.2 Network model
11.1.3 Workload characteristics
11.2 Dimensions of Concurrency control
11.2.1 Granularity
11.2.2 Mode
11.2.3 Lock Placement
11.3 The Coordination Lattice
11.4 Navigating the coordination lattice
11.4.1 Granularity selection
11.4.2 Mode selection
11.4.3 Placement selection
12 Experiments
12.1 Experimental setup
12.1.1 Inputs
12.1.2 Intermediate processes
12.1.3 DisLockSim – A simulation model for distributed lock
12.1.4 Cost of locking
12.2 Analysing some conflict graphs
12.2.1 Conflict graph involving two operations
12.2.2 Conflict graph involving three operations
13 Related work
14 Conclusion of Part III and Future work
14.1 Future work