Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Can you keep a secret? A new protocol for sender-side enforcement of causal message delivery

Yan Tong, Nathan Liittschwager, Lindsey Kuper

Abstract

Protocols for causal message delivery are widely used in distributed systems. Traditionally, causal delivery can be enforced either on the message sender's side or on the receiver's side. The traditional sender-side approach avoids the message metadata overhead of the receiver-side approach, but is more conservative than necessary. We present Cykas ("Can you keep a secret?"), a new protocol for sender-side enforcement of causal delivery that sidesteps the conservativeness of the traditional sender-side approach by allowing eager sending of messages and constraining the behavior of their recipients. We implemented the Cykas protocol in Rust and checked the safety and liveness of our implementation using the Stateright implementation-level model checker. Our experiments show that for applications involving long-running jobs, Cykas has a performance advantage: Cykas lets long-running jobs start (and end) earlier, leading to shorter overall execution time compared to the traditional sender-side approach.

Can you keep a secret? A new protocol for sender-side enforcement of causal message delivery

Abstract

Protocols for causal message delivery are widely used in distributed systems. Traditionally, causal delivery can be enforced either on the message sender's side or on the receiver's side. The traditional sender-side approach avoids the message metadata overhead of the receiver-side approach, but is more conservative than necessary. We present Cykas ("Can you keep a secret?"), a new protocol for sender-side enforcement of causal delivery that sidesteps the conservativeness of the traditional sender-side approach by allowing eager sending of messages and constraining the behavior of their recipients. We implemented the Cykas protocol in Rust and checked the safety and liveness of our implementation using the Stateright implementation-level model checker. Our experiments show that for applications involving long-running jobs, Cykas has a performance advantage: Cykas lets long-running jobs start (and end) earlier, leading to shorter overall execution time compared to the traditional sender-side approach.
Paper Structure (18 sections, 5 theorems, 3 equations, 6 figures, 1 table, 5 algorithms)

This paper contains 18 sections, 5 theorems, 3 equations, 6 figures, 1 table, 5 algorithms.

Table of Contents

  1. Introduction
  2. The Cykas Protocol
  3. Motivation: Bob's Long-Running Job
  4. Cykas in Detail
  5. Local data structures
  6. Protocol operation
  7. Why disallow sending in secret mode?
  8. Proof of Correctness
  9. Safety
  10. Liveness
  11. Bounded Verification
  12. Evaluation
  13. Experimental Setup
  14. Scalability of Sender-side vs. Receiver-side Protocols
  15. Cykas vs MFSS: Long-Running Job Performance Analysis
  16. ...and 3 more sections

Key Result

proposition 1

Any execution of Cykas with distinct send events $s^{m}$, $s^{m'}$ and corresponding receive-deliver events $\mathit{rd}^{m}$, $\mathit{rd}^{m'}$ satisfies causally ordered delivery.

Figures (6)

  • Figure 1: A violation of causal message delivery (left), and the receiver-side (center) and sender-side (right) approaches to preventing it. The send of message $m_1$ happens before the send of message $m_3$, thanks to the causal relationship created by the intervening message $m_2$. Causal delivery therefore mandates that Carol must deliver $m_1$ before $m_3$.
  • Figure 2: In our example execution, the delay imposed by the MFSS protocol is especially problematic (left) if Bob has a long-running job that he cannot begin until receiving $m_2$. However, eagerly sending $m_2$ in a naive way could lead to a violation of causal delivery (center). The Cykas protocol introduces the Eager Send and YCT message types, which can be used to let Bob get a head start on the long-running job (right).
  • Figure 3: If sending is allowed in secret mode, a causality violation can occur. ACK and YCT messages are elided in this figure.
  • Figure 4: Execution time comparison for the MFSS, Cykas, and matrix protocols at varying process-to-bandwidth ratios. With increasing process-to-bandwidth ratio, the matrix protocol's execution time increases quadratically.
  • Figure 5: Cykas speedup over MFSS across varying job characteristics (higher is better). Each subfigure shows a different communication frequency, with job length on the x-axis and Cykas speedup over MFSS on the y-axis (values > 1 indicate Cykas outperforms MFSS). Blue lines show execution time speedup, orange lines show average job start time speedup.
  • ...and 1 more figures

Theorems & Definitions (9)

  • proposition 1
  • proof
  • proposition 2
  • lemma 1
  • proof
  • lemma 2
  • proof
  • lemma 3
  • proof