http://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html

Skip to main content
 

Search This Blog

[                    ]
[Search]
Metadata

On distributed systems broadly defined and other curiosities. The
opinions on this site are my own.

Checking statistical properties of protocols using TLA+

  * Get link
  * Facebook
  * Twitter
  * Pinterest
  * Email
  * Other Apps

- October 03, 2022

In my previous post, I mentioned how excited I was about Jack
Vanlightly and Markus Kuppe's talk at TLA+ Conference. They showed a
new mode (called "generate") added to the TLA+ checker to enable 
obtaining statistical properties from the models. Here is how this
works in a nutshell. Your TLA+ model/protocol produces a tree of
runs, and, in the generate mode the TLA+ checker chooses these runs
in a uniform manner. You also specify some state constraints, and
when these are satisfied the TLA+ checker executes/evaluates your
state constraint formula: you add the statistics logging as the side
effect of this formula, and record information about the current run
to a CSV file. This way, you can collect statistical hyper properties
(abort rates, completion rounds, etc.) about the runs, in addition to
checking it for correctness invariants. Later you can use Excel or
Rscript to visualize the statistics collected and analyze the model
behavior.

Checking statistics is very useful, because ensuring correctness
addresses only one part of our concerns with practical systems.
Performance, availability, recovery speed are also important
dimensions of practical systems. We could of course write a Python
simulator and check these properties there, but then we would lose
the guarantees that the system is coded correctly (it is easy to
introduce bugs while translating the model). Doing these statistical
checks in TLA+ allows us to optimize and fine-tune the system all the
while preserving its safety-liveness properties via model checking.

This is so cool, and I thought I should learn this, and what better
way is there to learn something than trying it hands on using a
simple example. I chose Dijkstra's elegant self-stabilizing token
ring problem (EWD 426) as the example. Checking statistical
properties of this went well and easy. Of course, I botched it and
got stuck couple of times: Making mistakes is how we learn. I got
help from Markus to get unstuck, so the resulting model is joint work
with him. The model is available here under TLA+ examples.

I now have a decent understanding of how this works, and I look
forward to applying it to more complex models. The basic scheme is
very hackable and it is possible to extend statistics collection for
more ambitious efforts. Jack already gave some examples of applying
statistics checking to some SWIM, RabbitMQ, and Kafka models.


EWD 426: Stabilizing token ring protocol

EWD 426 is a simple protocol, but it is also a profound one. This
simple protocol, "Self-stabilizing systems in spite of distributed
control", started the entire field of stabilizing fault-tolerance.

I wrote about this protocol before and even gave a Pluscal model.
Here is how the protocol works.

The nodes/processes are arranged in a ring topology. The protocol
maintains a unique token circulating this ring. You can think of the
token as providing mutual exclusion to the processes; whichever
process has the token can access the critical-section/
shared-resource.

In the good/invariant states there is exactly one token. So in the
faulty states, there are two broad cases: 1) we end up with a ring
with no tokens,  2) we end up with a ring with multiple tokens.

Let's consider how Dijkstra's token ring algorithm deals with case 1.
Dijkstra's token ring algorithm maps the concept of a physical token
to a relation between two neighboring processes. This mapping is done
skillfully to limit the state space so the case 1 faults cannot
possibly happen in that state space. In the mapped state space, any
arbitrary state  is guaranteed to contain 1 or more tokens. How does
this work? Dijstra's algorithm encodes a token with the relation:
"the c variable of a process is DIFFERENT than the c variable of its
immediate predecessor in the ring". So, if all c variables are the
same, there won't be any token in the system. To prevent this, the
algorithm encodes the token differently for process 0: "There is a
token at process 0, if its c variable is the SAME as that of its
predecessor, process N". Encoded this way, we cannot not have 0
tokens in any arbitrary state in the state space.

In order to deal with case 2, Dijkstra's algorithm uses a token
overwriting action to eat some tokens on a best effort fashion. The
action is to copy the c value of your predecessor, when your c value
is different than its c value (hence, you have the token). In the
normal/fault-free case, by taking an action a process consumes a
token that exists between its predecessor and itself and passes this
token to its successor. In the faulty states case, this is also the
worst damage the action can do, because the process will always
consume the token at itself, and since its state change affects only
its successor, it may or may not pass the token to its successor. If
the process execution does not pass the token to its successor, this
is actually good: two tokens are removed from the system (one between
it and its predecessor, and the other between it and its successor).
If enough of these remove token behavior happens, the system will
stabilize to exactly one token case.

But what if the remove token behavior leads to a system with no
tokens? Recall that this cannot happen due to the discussion
regarding Case 1.


Stabilizing token ring model

The Pluscal version is fine, but I wanted to give a clean and simpler
TLA+ version. I was inspired by the slick VSCode interface Markus
demoed to me earlier in the TLA+ conference to write clean solid
engineered code. If written cleanly, TLA+ models are easy to read. (I
am channeling the Paxos Made Simple abstract.)


[AVvXsEjZLp]

Above is the model. I make the nodes start with arbitrary c values in
line 23, since I like to model check stabilization to a unique token.
Line 26 is the CreateToken action, which only process 0 executes. It
is enabled if c[0] = c[N-1], and it sets c[0] to C[N-1]+1 in modulo
M.

Line 31 is the PassToken action executed by processes that are not
process 0. This is enabled if the predecessor has a different c value
than the node c [i] # c [i-1], and this copies the value of c[i-1] to
c[i].

[AVvXsEiaXl]

In the invariant states, there is only one token in the system. The
two-line UniqueToken predicate captures this property. It says that
unique token is true iff there exists a node i such that

  * for all nodes from 0 to i, c values are equal to the c value of
    0, and
  * for all nodes from i to N-1, c values are equal to c[0] -1 in
    modulo M.

Here N is the number of nodes in the ring: 0..N-1. And M is the bound
on the c value. We wrap the c value around when it reaches M, because
we cannot use unbounded integers in our implementation so we have
bounds on c. There is an interesting dynamic between M and N, which I
will mention below.


Model checking EWD 426

The .cfg file carries the configuration of the model checking. Using
the TLA+ toolkit, it was frustrating not to be able to give the model
checking instructions well. I would use the comments to say that you
can instantiate the model with these constants, and you can use the
following properties for model checking. But several things would
still be missing, like whether we turn off deadlock checking or not.
Now, this cfg file captures all the model checking parameters. This
is also version control friendly. If the name of the cfg file is the
same as the tla file, it will automatically get picked up by the TLA+
checker. With developers using TLA+ more and more, the TLA+ tools
improved significantly to cater to the development best practices.

[AVvXsEi4O7]

So here is the .cfg for model checking EWD 426. I will change this
slightly for statistics collection (there I will un-comment the state
constraints line).

Since EWD426 is supposed to show case stabilization, I make the
system start in an arbitrary state (see line 23) and check that it
stabilizes to invariant states. So I am  not checking UniqueToken as
the invariant, clearly it would be violated at the start. Instead, I
am model checking stabilization to UniqueToken. This is very easy to
write. Stab  == <>[] UniqueToken

Relation between M and N

If we choose M<N-1, we lose stabilization. Check it yourself to see
how this happens. TLA+ will give you a counterexample where a
looped-execution is able to keep more than one token in the system
forever. In this execution, Node 0 is tricked into creating a new
token ad infinitum, when there is already a token somewhere in the
inner nodes.

At M=N-1 (or above), a phase transition happens. The node 0 is now
able to act as a gate. Consider the case where node 0 never fires. In
this case the other nodes fire, and eventually they all copy the c
value at node 0, and in that configuration the system reduces to one
token (at node 0) and stabilization is achieved. For M=N-1 and above,
the pigeon-hole principle applies to show that the c value of Node 0
eventually reaches a different value than in the inner nodes, and 
node 0 does not fire until all other nodes  copy its value. 


Setting up for checking statistics

Here is the easiest way to set up your laptop for TLA+ statistics
checking. Install the TLA+ nightly build VSCode extension. The
statistics checking is only available in the nightly build extension.

When you are model checking, bring up the command palette by pressing
option-X, and select "TLA+ Check Model with TLC" and enter "-coverage
1", so that the checker will report on its model checking progress
back to you every minute.

When you are checking statistics, you do the same thing again. Press
option-X,  and select "TLA+ Check Model with TLC". But this time you
will enter a different prompt: "-generate -depth N". The generate
mode is recently added: in this mode the TLA+ checker chooses enabled
actions in a uniformly random manner and executes sample runs from
your model one after the other.

N is an integer. N=-1 this means that the TLA+ checker executes each
run until deadlock, and then moves to new run. N=50 means that the
TLA+ checker will execute each run upto 50 steps deep, then move to a
new run.

Now, I uncomment the state constraints line in the cfg file, and we
are ready to check statistics for EWD 426.
 

Mechanics of statistics collection

The core of idea in logging/collecting statistics is to State/Action
constraints as a hook to record statistics from each run to a CSV
file. Recording every action in a run would not be useful. You want
to record when something significant occurs. TLA+ let's you write
state predicates and action properties to capture any interesting
stuff you can think of. 

Originally, the TLA+ checker used these constraints to stop exploring
a run when the execution is not desirable anymore. Now we hijack the
same mechanism, and use the side effects of the state/action
constraints to perform statistics collection. Here is the state
constraint I added to collect statistics.
[AVvXsEhf-E]

This is a hook that is run for each state encountered. The left hand
side of the implication evaluates the UniqueToken predicate on the
current global state the TLA+ checker encountered in this particular
run. If UniqueToken does not hold, the left hand side becomes FALSE,
and makes the implication statement TRUE, so the state constraint
returns TRUE. The right-hand side is not even evaluated because the
left-hand-side is FALSE. Returning TRUE means the run will continue
to the next state. The TLA+ checker chooses another enabled action
uniformly random and evaluates the StateConstraint on the new state
found.

When UniqueToken holds for a state, the right-hand side of the
implication is taken. Here we use TLCGet to get "level", which
indicates the current depth of steps in to this particular run, when
UniqueToken is truthified. CSVWrite adds this line of statistics into
the CSVFile we denoted earlier. For this to work, we imported CSV in
the EXTENDS line.

When UniqueToken holds, we like to stop exploring so we add
conjunction FALSE to the right hand side, making the expression
return FALSE (after having done the CSVWrite side effect). FALSE
tells the checker to stop exploring this particular run, because we
got to where we wanted. (I had previously model-checked and ensured
that the system always stabilizes, I am not interested in exploring
this run to check UniqueToken keeps holding.)

That is how statistics collection works. We invoke this generate mode
writing "-generate -depth -1" and let it rip through sampling the
runs and collecting statistics.  When we stop the TLA checker after a
minute, we will have tens of thousands of runs, and hence that many
entries in our CSV file. The rest is up to us to process/visualize
this data. Use excel if you like. But a more programmatic way of
doing this is to use Rscript and write visualizations to an image
file, like svg.

We can do this visualization offline, or using a clever hack Markus
devised online, while TLA+ checker is running and exploring the runs.
Just append this to AtStabilization state constraint. TLCGet("stats")
provides information like how many of each action is executed in a
run, how many runs has been explored, etc. This line invokes Rscript
on the CSV file after every 250 runs explored. Each time it is
invoked, Rscript regenerates the svg image, and using the svg viewer
in VSCode, we see the statistics changing in real time.   
[AVvXsEg7dc]

Here is a screen recording for N=7 and M=6 configuration.
 


There is also TLCSet command, which can give you more flexibility in
logging/collecting statistics. TLCSet can be used to store things to
a register, registers are numbered starting from 1. Later you can
TLCGet that register to read what you memorized earlier in this
particular run, or even in previous runs. Markus showed an example of
this in his Termination Detection model.

Analysis

Let's check the statistics we collected. Here is the histogram for N=
7 and M=6 configuration. There is a nice uniform distribution of
number of steps required for stabilization. 10 steps seem to be the
average. There is a bump at step 1, but this is due to some initial
states being those for which UniqueToken already holds.
[AVvXsEgAKv]
We know M=2 that is modulo binary doesn't work, we go to a loop to
easily. Even in the generate mode with depth 50, the TLA+ checker
complains, saying a loop is detected and stabilization does not
occur. "Error: Temporal properties were violated. Error: The
following behavior constitutes a counter-example."

But for M=3, this works, because probabilistically it is hard to hit
the looping run here. This makes the average stabilization at 8-9
steps and skews the distribution toward the left, and somehow makes
the tail more pronounced. That is not much of an improvement.
Although we capped the M domain, the N domain still throws us
significant number of state configurations. Since there are many
nodes whose states need to be fixed and aligned globally.
[AVvXsEh_Uz]

The theoretical worst case for stabilization of EWD 426 is M*N. For N
=7 and M=6 that makes 42, but we see that in practice stabilization
occurs much earlier. And for N=7 and M=3 (an unsafe configuration),
we don't see significant improvement in stabilization time over the
safe configuration.


Debugging via TLA+

Of course I didn't get the TLA+ model work in one shot. I had made
boundary condition errors in definition of UniqueToken. The VSCode
TLA+ checker now includes debugging support and that helped me.
Markus shared a video about this recently. Markus added this support
in a generalizable way through Debug Adapter Protocol (DAP), so the
community can extend the debugging support to Intellij and CLI.  

What blew my mind in the debuggin mode was that if you add a
breakpoint in the Spec line and run TLC in Debug mode using -simulate
prompt, you can use the VSCode debug menu to skip over an action or
step into that action, backtrack and move forward again. This way you
can control how the run goes, navigate it to particular tricky
situations and see what goes there.

Another cool trick is to add an ALIAS in the cfg file, to improve how
debugging information is presented to you. Instead of raw state
debuggging, you can make the definitions work for you and provide you
the predicates you care about the raw state. Here is the alias
predicate I used to get a high level view of the state.
[AVvXsEgtFn]
 
stabilization statistics tla

  * Get link
  * Facebook
  * Twitter
  * Pinterest
  * Email
  * Other Apps

Comments

Post a Comment

Popular posts from this blog

Graviton2 and Graviton3

- December 04, 2021
Image
What do modern cloud workloads look like? And what does that have to
do with new chip designs? I found these gems in Peter DeSantis's
ReInvent20 and ReInvent21 talks. These talks are very informative and
educational. Me likey! The speakers at ReInvent are not just
introducing new products/services, but they are also explaining the
thought processes behind them. To come up with this summary, I edited
the YouTube video transcripts slightly (mostly shortening it). The
presentation narratives have been really well planned, so this makes
a good read I think. Graviton2 This part is from the ReInvent2020
talk from Peter DeSantis.   Graviton2 is the best performing general
purpose processor in our cloud by a wide margin. It also offers
significantly lower cost. And it's also the most power efficient
processor we've ever deployed. Our plan was to build a processor that
was optimized for AWS and modern cloud workloads. But, what do modern
cloud workloads look like? Let's start by
 
Read more >>

Foundational distributed systems papers

- February 27, 2021
I talked about the importance of reading foundational papers last
week. To followup, here is my compilation of foundational papers in
the distributed systems area. (I focused on the core distributed
systems area, and did not cover networking, security, distributed
ledgers, verification work etc. I even left out distributed
transactions, I hope to cover them at a later date.)  I classified
the papers by subject, and listed them in chronological order. I also
listed expository papers and blog posts at the end of each section.
Time and State in Distributed Systems Time, Clocks, and the Ordering
of Events in a Distributed System. Leslie Lamport, Commn. of the
ACM,  1978. Distributed Snapshots: Determining Global States of a
Distributed System. K. Mani Chandy Leslie Lamport, ACM Transactions
on Computer Systems, 1985. Virtual Time and Global States of
Distributed Systems.  Mattern, F. 1988. Expository papers and blog
posts There is No Now . Justin Sheehy, ACM Queue 2015 Why Logical
Clock
 
Read more >>

Learning a technical subject

- December 18, 2021
I love learning. I wanted to write about how I learn, so I can
analyze if there is a method to this madness. I will first talk about
what my learning process looks like in abstract terms, and then I'll
give an analogy to make things more concrete and visual.   Learning
is a messy process for me I know some very clear thinkers. They are
very organized and methodical. I am not like that. These tidy
thinkers seem to learn a new subject quickly (and effortlessly) by
studying the rules of the subject and then deriving everything about
that subject from that set of rules. They speak in precise statements
and have clear and hard-set opinions about the subject. They seem to
thrive most in theoretical subjects. In my observation those tidy
learners are in the minority. Maybe the tidy thinkers are able to
pull this feat off because they come from a neighboring domain/
subject and map the context there to this subject quickly. But, again
from my experience, it doesn't feel like that. It s
 
Read more >>

SQLite: Past, Present, and Future

- September 19, 2022
Image
SQLite is the most widely deployed database engine (or likely even
software of any type) in existence. It is found in nearly every
smartphone (iOS and Android), computer, web browser, television, and
automobile. There are likely over one trillion SQLite databases in
active use. (If you are on a Mac laptop, you can open a terminal,
type "sqlite3", and start conversing with the SQLite database engine
using SQL.) SQLite is a single node and (mostly) single threaded
online transaction processing (OLTP) database. It has an in-process/
embbedded design, and a standalone (no dependencies) codebase ...a
single C library consisting of 150K lines of code.  With all features
enabled, the compiled library size can be less than 750 KiB. Yet,
SQLite can support tens of thousands of transactions per second. Due
to its reliability, SQLite is used in mission-critical applications
such as flight software. There are over 600 lines of test code for
every line of code in SQLite. SQLite is truly t
 
Read more >>

Learning about distributed systems: where to start?

- June 10, 2020
This is definitely not a "learn distributed systems in 21 days" post.
I recommend a principled, from the foundations-up, studying of
distributed systems, which will take a good three months in the first
pass, and many more months to build competence after that. If you are
practical and coding oriented you may not like my advice much. You
may object saying, "Shouldn't I learn distributed systems with coding
and hands on? Why can I not get started by deploying a Hadoop
cluster, or studying the Raft code." I think that is the wrong way to
go about learning distributed systems, because seeing similar code
and programming language constructs will make you think this is
familiar territory, and will give you a false sense of security. But,
nothing can be further from the truth. Distributed systems need
radically different software than centralized systems do.  --A.
Tannenbaum This quotation is literally the first sentence in my
distributed systems syllabus. Inst
 
Read more >>

Strict-serializability, but at what cost, for what purpose?

- August 03, 2022
Image
Strict-serializability guarantees that transactions appear to occur
in an order consistent with the "real-time" ordering of those
transactions: If transaction T1 commits before transaction T2 is
invoked, then the commit timestamp of T1 precedes the commit
timestamp of T2. This is, in fact, the real-time constraint from
linearizability , but applied across transactions not just per-key. A
strict-serializability system satisfies both serializability
(transactions appear to occur as if they are executed one at a time
in isolation) and linearizability per key (after all single-key reads
/writes are transactions over one item). Below figure is from https:/
/jepsen.io/consistency . However, this is a one-way implication, the
other direction does not hold. You can satisfy both serializability
per transactions and linearizability per key, but fail to satisfy
strict-serializability. (Below I give an example accompanied with a
TLA+ specification to check it.) This is because, in strict-
 
Read more >>

CockroachDB: The Resilient Geo-Distributed SQL Database

- March 04, 2022
Image
This paper appeared in Sigmod 2020. Here is a link to the 10 minute,
but extremely useful, Sigmod presentation . There is also a 1 hour
extended presentation . CockroachDB is open source available via
GitHub. The core features of the database are under a Business Source
License (BSL), which converts to a fully open-source Apache 2.0
license after three years. Storage layer CockroachDB (or CRDB for
short) consists of a distributed SQL layer on top of a distributed
key-value store. The key value store is laid out in a single
monolithic ordered key space. The logical key space is physically
realized by dividing it into contiguous ranges of keys which we call
ranges. Ranges are about 64 megabytes in size. Ranges start empty,
grow, and split when they get too large, and merge with their
neighbors when they get too small. The ranges are sorted, and I will
talk about why in the SQL discussion later. As we will discuss soon,
CRDB uses multi-version concurrency control. Hybrid logical clocks
 
Read more >>

The Seattle Report on Database Research (2022)

- August 08, 2022
Every 5 years, researchers from academia and industry gather to write
a state-of-the-union (SOTU) report on database research. This one was
released recently . It is a very readable report, and my summary
consists of important paragraphs clipped from the report. Emphasis
mine in bolded sentences. I use square brackets for when I paraphrase
a long text with a more direct statement. TL;DR: The SOTU is strong
(the relational database market alone has revenue upwards of $50B)
and growing stronger thanks to boom in cloud computing and machine
learning (ML). For the next 5 years, research should scale up to
address emerging challenges in data science, data governance, cloud
services, and database engines.   What has changed in the last 5
years Over the last decade, our research community pioneered the use
of columnar storage, which is used in all commercial data analytic
platforms. Database systems offered as cloud services have witnessed
explosive growth. Hybrid transactional/analytical pro
 
Read more >>

Amazon Aurora: Design Considerations + On Avoiding Distributed
Consensus for I/Os, Commits, and Membership Changes

- March 20, 2022
Image
Amazon Aurora is a high-throughput cloud-native relational database.
I will summarize its design as covered by the Sigmod 17 and Sigmod 18
papers from the Aurora team. Aurora uses MySQL or PostgreSQL for the
database instance at top, and decouples the storage to a multi-tenant
scale-out storage service.  In this decoupled architecture, each
database instance acts as a SQL endpoint and supports query
processing, access methods, transactions, locking, buffer caching,
and undo management. Some database functions, including redo logging,
materialization of data blocks, garbage collection, and backup/
restore, are offloaded to the storage nodes. A big innovation in
Aurora is to do the replication among the storage nodes by pushing
the redo log; this reduces networking traffic and enables
fault-tolerant storage that heals without database involvement. In
contrast to CockroachDB and FoundationDB , Aurora manages not to use
consensus at all. It uses a primary secondary failover at the comp
 
Read more >>

Warp: Lightweight Multi-Key Transactions for Key-Value Stores

- May 04, 2022
Image
This paper introduces a simple yet powerful idea to provide efficient
multi-key transactions with ACID semantics on top of a sharded NoSQL
data store. The Warp protocol prevents serializability cycles forming
between concurrent transactions by forcing them to serialize via a
chain communication pattern rather than using a parallel 2PC fan-out/
fan-in communication. This avoids hotspots associated with fan-out/
fan-in communication and prevents wasted parallel work from
contacting multiple other servers when traversing them in serial
would surface an invalidation/abortion early on in the serialization.
I love the elegance of this idea. As far as I can see, this paper did
not get published in any conference. The authors published a followup
paper to this in NSDI 16, called "The Design and Implementation of
the Warp Transactional Filesystem." But that paper does not talk
about the internals of Warp protocol like this archive report, rather
talks about the Warp Transactional File
 
Read more >>
Powered by Blogger
Theme images by Michael Elkan
Murat Demirbas
My photo

Murat
    I am a principal applied scientist at AWS. On leave as a computer
    science and engineering professor at SUNY Buffalo. I work on
    distributed systems, distributed consensus, and cloud computing.
    You can follow me on Twitter.

Visit profile

Pageviews

Recent Posts

  * October1
  * September4
  * August5
  * July6
  * June3
  * May3
  * April4
  * March3
  * February3
  * January3

  * December5
  * November3
  * October6
  * September1
  * August4
  * July2
  * June12
  * May1
  * April1
  * March4
  * February4
  * January4
  * December3
  * November7
  * October4
  * September1
  * August3
  * July6
  * June11
  * May9
  * April8
  * March8
  * February7
  * January9
  * December10
  * November14
  * October6
  * September13
  * July3
  * June3
  * May4
  * April6
  * March2
  * February1
  * January3
  * December4
  * November7
  * October2
  * September2
  * August8
  * July2
  * June4
  * May9
  * April6
  * March9
  * February5
  * January13
  * December15
  * November15
  * October5
  * September8
  * August10
  * July3
  * June3
  * May3
  * April4
  * February4
  * January7
  * December7
  * November9
  * October3
  * September1
  * July4
  * June5
  * May1
  * April4
  * March2
  * February2
  * January4
  * December3
  * November2
  * October3
  * September2
  * August3
  * June1
  * May1
  * April6
  * March6
  * February4
  * January3
  * November4
  * October4
  * September6
  * August2
  * July2
  * June3
  * March3
  * February4
  * January1
  * December1
  * November2
  * August2
  * July4
  * June2
  * May5
  * April8
  * January1
  * December1
  * November7
  * October1
  * September2
  * August1
  * May2
  * March1
  * February1
  * January2
  * December3
  * September5
  * June1
  * May5
  * April5
  * March5
  * February9
  * January5
  * December6
  * November9
  * October9
  * September7
  * August1

Show more Show less

Topics

analytics1 auditability5 automated reasoning5 aws1 Azure10 benchmarks
1 bestof5 big-data23 Blockchain39 book-review49
chaos2 cloud computing6 consistency24 Cosmos DB10 CosmosDB11 data
warehouse1 databases22 dataflow7 disaggregation1 distributed
consensus42 distributed transactions17 distSQL4 facebook15 failures16
fault-tolerance37 formal methods11 graph-processing1 htap1 humans10 
indexing3 isolation levels1 links2 mad-questions42 main-memory1 misc
102 mlbegin7 mldl25 mobile2 my advice15 my-paper10 newsql2 OLAP1 
paper-review144 paxos46 presenting4 programming5 reading-group23 
research-advice47 research-question43 Rust3 scheduling3 seminar9 
serializability1 serverless1 smartphones2 snapshot isolation1 
sonification1 SQL1 stabilization6 statistics1 stream-processing10 
teaching30 tensorflow11 time8 time synchronization1 tla41 
transactions5 trip-report23 wpaxos5 writing26
Show more Show less