240 lines
16 KiB
HTML
240 lines
16 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1"><!-- Begin Jekyll SEO tag v2.8.0 -->
|
||
<title>User settings, Lamport clocks and lightweight formal methods | Jakub Mikians blog</title>
|
||
<meta name="generator" content="Jekyll v3.10.0" />
|
||
<meta property="og:title" content="User settings, Lamport clocks and lightweight formal methods" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Synchronizing settings between browsers and a backend seems a simple task. It turns out that it can teach us some lessons on distributes systems and formal modeling. After you read this post, you will learn, I hope, how we used Lamport Clocks to synchronize user settings between browsers and backend service. You will also learn how we used Lightweight Formal Methods to find bugs in our implementation of the synchronization protocol." />
|
||
<meta property="og:description" content="Synchronizing settings between browsers and a backend seems a simple task. It turns out that it can teach us some lessons on distributes systems and formal modeling. After you read this post, you will learn, I hope, how we used Lamport Clocks to synchronize user settings between browsers and backend service. You will also learn how we used Lightweight Formal Methods to find bugs in our implementation of the synchronization protocol." />
|
||
<link rel="canonical" href="https://jakub-m.github.io/2022/07/17/laport-clocks-formal.html" />
|
||
<meta property="og:url" content="https://jakub-m.github.io/2022/07/17/laport-clocks-formal.html" />
|
||
<meta property="og:site_name" content="Jakub Mikians blog" />
|
||
<meta property="og:type" content="article" />
|
||
<meta property="article:published_time" content="2022-07-17T21:46:39+00:00" />
|
||
<meta name="twitter:card" content="summary" />
|
||
<meta property="twitter:title" content="User settings, Lamport clocks and lightweight formal methods" />
|
||
<script type="application/ld+json">
|
||
{"@context":"https://schema.org","@type":"BlogPosting","dateModified":"2022-07-17T21:46:39+00:00","datePublished":"2022-07-17T21:46:39+00:00","description":"Synchronizing settings between browsers and a backend seems a simple task. It turns out that it can teach us some lessons on distributes systems and formal modeling. After you read this post, you will learn, I hope, how we used Lamport Clocks to synchronize user settings between browsers and backend service. You will also learn how we used Lightweight Formal Methods to find bugs in our implementation of the synchronization protocol.","headline":"User settings, Lamport clocks and lightweight formal methods","mainEntityOfPage":{"@type":"WebPage","@id":"https://jakub-m.github.io/2022/07/17/laport-clocks-formal.html"},"url":"https://jakub-m.github.io/2022/07/17/laport-clocks-formal.html"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/assets/main.css"><link type="application/atom+xml" rel="alternate" href="https://jakub-m.github.io/feed.xml" title="Jakub Mikians blog" /></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper"><a class="site-title" rel="author" href="/">Jakub Mikians blog</a><nav class="site-nav">
|
||
<input type="checkbox" id="nav-trigger" class="nav-trigger" />
|
||
<label for="nav-trigger">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.032C17.335,0,18,0.665,18,1.484L18,1.484z M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.032C17.335,6.031,18,6.696,18,7.516L18,7.516z M18,13.516C18,14.335,17.335,15,16.516,15H1.484 C0.665,15,0,14.335,0,13.516l0,0c0-0.82,0.665-1.483,1.484-1.483h15.032C17.335,12.031,18,12.695,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
</label>
|
||
|
||
<div class="trigger"><a class="page-link" href="/about/">About</a></div>
|
||
</nav></div>
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post h-entry" itemscope itemtype="http://schema.org/BlogPosting">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title p-name" itemprop="name headline">User settings, Lamport clocks and lightweight formal methods</h1>
|
||
<p class="post-meta">
|
||
<time class="dt-published" datetime="2022-07-17T21:46:39+00:00" itemprop="datePublished">Jul 17, 2022
|
||
</time></p>
|
||
</header>
|
||
|
||
<div class="post-content e-content" itemprop="articleBody">
|
||
<p>Synchronizing settings between browsers and a backend seems a simple task. It turns out that it can teach us some
|
||
lessons on distributes systems and formal modeling. After you read this post, you will learn, I hope, how we used
|
||
<a href="https://martinfowler.com/articles/patterns-of-distributed-systems/lamport-clock.html">Lamport Clocks</a> to synchronize user settings between browsers and backend service. You will also learn
|
||
how we used <a href="https://dl.acm.org/doi/10.1145/3477132.3483540">Lightweight Formal Methods</a> to find bugs in our implementation of the synchronization
|
||
protocol.</p>
|
||
|
||
<p>At <a href="https://www.airspace-intelligence.com/company">Airspace Intelligence</a> we work on products supporting airlines’ operations. One of the products we are
|
||
building is an application for messaging between the dispatchers (the ground staff coordinating the carriers’
|
||
aircrafts), and the pilots (the folks driving the planes). Think of WhatsApp for airplanes.</p>
|
||
|
||
<p>The application, or just the App, integrates with the <a href="https://en.wikipedia.org/wiki/ACARS">existing airline’s systems</a>. The App delivers slick
|
||
browser UI, and at the same time needs to communicate with the existing notification systems to notify that the
|
||
dispatcher has a new message from the pilot. The “existing notification systems” are not browser-based, so even though
|
||
the messaging itself happens in the browser, the notification flow happens outside of the browser. Think of
|
||
push notifications that are delivered to a device outside browser. To deliver messages to proper users (e.g. all the
|
||
dispatchers interested in flights departing from Seattle), the backend service relies on the user settings to figure
|
||
out which user (dispatcher) should be notified about which message. Different dispatchers handle a different set of flights.</p>
|
||
|
||
<p>It is important that the browsers serving the App, connected to the backend, and the backend itself, have a consistent
|
||
view on the user settings, so the backend can reliably trigger send notifications to the dispatchers about pending
|
||
messages. The case we especially want to avoid is that the browsers “see” different settings than the backed, or that
|
||
the settings between the browsers and the backend don’t converge. At the same time, we want to provide a snappy
|
||
experience, when the dispatcher can select different settings (different flight selectors), and the settings won’t
|
||
flicker as the requests and responses go back and forth between the browser and the backend.</p>
|
||
|
||
<h1 id="but-thats-trivial-right">But that’s trivial, right?</h1>
|
||
|
||
<p>Superficially yes. But if you want to be <em>sure</em> that the settings are synchronized correctly, avoid weird edge cases
|
||
and still provide a snappy experience, you need to take extra care.</p>
|
||
|
||
<p>With two browsers and a single backend (single storage), different things can happen. A user can click settings in one
|
||
browser, and then different settings in another one. There can be transient network problems so the browsers fail to
|
||
send the up-to-date settings to the backend. The user can click back and forth the settings several times, or restart the
|
||
browser.</p>
|
||
|
||
<p>The simplest thing to do would be to send the settings with each click. The problem is that if you clicked different
|
||
settings fast, or when the network is slow, it could happen that you changed some setting A and then a different
|
||
settings B, but after you clicked B your browser received a response from the backend for “A” change. The “A response”
|
||
would overwrite the “B” change in the browser, causing the settings to flicker. Alternatively, you could wait for a response
|
||
after each request, but then the experience wouldn’t be “snappy”.</p>
|
||
|
||
<p>Also, what if your request never reached the backend service? Aha, you say, let’s add a periodic sync job in the
|
||
browser to synchronize the state of the browser with the backend. This would also protect us from the case when someone
|
||
changed settings in a different browser window. This would work, but you need to figure which settings are the “current”
|
||
ones, the ones in the browser or the ones on the backend. Easy, just add a clock. But now how can you be <em>sure</em> that the
|
||
clock is right? It should, <a href="https://phys.org/news/2012-07-wreaks-internet-havoc.html">but what if not</a>? How can you reliably <a href="https://sookocheff.com/post/time/lamport-clock/">compare the clocks</a>?
|
||
Folk wisdom says to never trust external clocks.</p>
|
||
|
||
<p>You could add some integer that you increment every time you synchronize or change state, and choose the larger one…
|
||
Wait, sounds like you are inventing the…</p>
|
||
|
||
<h1 id="lamport-clocks">Lamport Clocks</h1>
|
||
|
||
<p>The idea is straightforward: make each process measure its own time, and synchronize the time when the processes
|
||
(browsers and the backend) exchange events.</p>
|
||
|
||
<p>Events make the time “tick”. When an event, like a change in the settings, happens, a process increments its local time
|
||
(an integer). When the processes exchange the information, they pass the counter along, compare the received counter
|
||
with the local counter, choose the larger one (local or received) together with the accompanying state (i.e. the
|
||
settings), <em>and increment the local clock by 1</em>. Mr. Lamport showed that such clocks allow reasoning about the <a href="https://en.wikipedia.org/wiki/Lamport_timestamp">ordering
|
||
of the events</a>.</p>
|
||
|
||
<p>Each time the user clicks the settings, the Lamport clock (a local integer) in the browser increments by 1. The settings
|
||
are sent from the browsers to the backend, and the “larger clock wins”. Eventually, all the browsers and the backend
|
||
should converge to the same values… At least that’s what we thought.</p>
|
||
|
||
<h1 id="lightweight-formal-methods">Lightweight formal methods</h1>
|
||
|
||
<p>Testing a distributed system, even as simple as the above, is difficult. There are <a href="https://en.wikipedia.org/wiki/TLA%2B">dedicated frameworks and languages,
|
||
like TLA+</a> for that purpose. While expressive and battle-proven, a “test”, or specification, written in
|
||
TLA+ would be doomed to become instantly unmaintained. Instead, we adopted “Property-based testing” described in the
|
||
<a href="https://dl.acm.org/doi/10.1145/3477132.3483540">Lightweight Formal Methods</a> paper. In a nutshell, the idea is that you implement simple reference
|
||
models, then randomly generate sets of events, and check if after running the events on the reference models the
|
||
properties of the system hold. Such “lightweight formal tests” are a part of the regular unit-test suite, together with
|
||
the other tests.</p>
|
||
|
||
<p>In our case, a “reference model” for a browser app was merely a class with two fields - “settings” and “Lamport clock”.
|
||
The backend service used in the tests was the <em>actual</em> backend service running locally as a part of the unit test setup.</p>
|
||
|
||
<p>The events generated were:</p>
|
||
|
||
<ol>
|
||
<li>The user changed settings in the app and the app sent the up-to-date settings to the backend.</li>
|
||
<li>The user changed settings but the browser did not send the up-to-date settings to the backend (e.g. because of
|
||
the connectivity issues).</li>
|
||
<li>The browser synchronizes with the backend.</li>
|
||
<li>The browser resets.</li>
|
||
</ol>
|
||
|
||
<p>What we tested for was the property: after a random set of events and two synchronization rounds between the browsers
|
||
and the backend, all the browsers and the backend had the same settings. We used “two synchronization rounds” as it
|
||
turned out that one synchronization round is not enough for convergence.</p>
|
||
|
||
<h1 id="the-bug">The bug</h1>
|
||
|
||
<p>So we run the test with thousands and thousands of sequences of events, and, to our surprise, the tests failed! There
|
||
was a sequence of events that caused the system to not converge to a single state. It turned out that
|
||
the state would not converge when all of the browsers and the backend had different settings but the same values of Lamport
|
||
clocks. Consider the following sequence:</p>
|
||
|
||
<ol>
|
||
<li>Initial state.
|
||
<ul>
|
||
<li>browser: settings: none, clock: 0</li>
|
||
<li>backend: settings: none, clock: 0</li>
|
||
</ul>
|
||
</li>
|
||
<li>The user changes settings in the browser, and the browser synchronizes the settings with the backend. The clock for
|
||
browser is 3: just after the settings change, locally the clock increments to 1, is sent to the backend, the backend
|
||
increments the clock to 2, and sends it to the browser where it is yet again incremented to 3.
|
||
<ul>
|
||
<li>browser: settings: foo, clock: 3</li>
|
||
<li>backend: settings: foo, clock: 2</li>
|
||
</ul>
|
||
</li>
|
||
<li>The browser resets, all the state is dropped.
|
||
<ul>
|
||
<li>browser: settings: none, clock: 0</li>
|
||
<li>backend: settings: foo, clock: 2</li>
|
||
</ul>
|
||
</li>
|
||
<li>The user changes the settings twice, but this time the state is not propagated to the backend (e.g. due to network
|
||
hiccups).
|
||
<ul>
|
||
<li>browser: settings: none, clock: 2</li>
|
||
<li>backend: settings: foo, clock: 2</li>
|
||
</ul>
|
||
</li>
|
||
</ol>
|
||
|
||
<p>Now, if left like that, the state would never converge between the browser and the backend. Both ends have the same clock
|
||
value and cannot decide on the order of the events. Rare? Yes, rare. Correct? Definitely not!</p>
|
||
|
||
<p>The fix was to break the tie by incrementing the clock on the backend side whenever comes a request with the equal clock.
|
||
Intuitively, one can argue that something might have happened on the backend side meanwhile, e.g. settings changed to
|
||
some value and changed back to the original value, leaving the settings unchanged but the clock incremented. With the
|
||
above example, when the backend received an event with the browser clock value equal to the backend’s local clock value,
|
||
the backend would silently increment its clock and return it to the browser:</p>
|
||
|
||
<ol start="5">
|
||
<li>Backend increments its clock on an equal input clock.
|
||
<ul>
|
||
<li>browser: settings: none, clock: 4</li>
|
||
<li>backend: settings: foo, clock: 3</li>
|
||
</ul>
|
||
</li>
|
||
</ol>
|
||
|
||
<p>After the change, the test didn’t fail anymore.</p>
|
||
|
||
<h1 id="conclusions">Conclusions</h1>
|
||
|
||
<p>Handling even a simple distributed state is not trivial if one wants to do it correctly. Fortunately, algorithms and rich
|
||
research exist. Lightweight formal testing is a very <em>practical</em> framework for testing such algorithms in the
|
||
application context.</p>
|
||
|
||
<p>(<a href="https://news.ycombinator.com/item?id=32171619">on HN</a>)</p>
|
||
|
||
|
||
</div><a class="u-url" href="/2022/07/17/laport-clocks-formal.html" hidden></a>
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Jakub Mikians blog</h2>
|
||
|
||
<div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jakub Mikians blog</li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jakub-m"><svg class="svg-icon"><use xlink:href="/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jakub-m</span></a></li><li><a href="https://mastodon.social/@jakubm"><svg class="svg-icon"><use xlink:href="/assets/minima-social-icons.svg#mastodon"></use></svg> <span class="username">jakubm</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3">
|
||
<p>An exercise in writing. All the opinions are mine, unless you share them.</p>
|
||
</div>
|
||
</div>
|
||
|
||
</div>
|
||
|
||
</footer>
|
||
</body>
|
||
|
||
</html>
|