|
-------------------------------------------------------------
POPL 19
-------------------------------------------------------------
This work strikes a sweet spot in a crowded and noisy design space in
which many different approaches have been proposed to allow users to
commit to a single consistency model for their entire application, or
fine-tune or otherwise adjust or balance the consistency requirements
of portions of their applications. Other work has proposed tools or
programming models focused on one of the various flavors of consistency
(strong, eventual, causal...) but few come close to providing an
automatic solution that can so convincingly work out conflicting
operations (requiring synchronization) or dependent operations
(requiring causality) or independent operations (coordination-free) and
then instantiate the appropriate protocols for each operation,
resulting in an object that can be freely and correctly replicated.
Further, the idea to reduce the coordination avoidance problem to a
regular graph optimization problem is excellent, and key to the success
of the approach.
This work seems well-poised to make a substantial impact in the design
and implementation of distributed systems going forward, and I think it
would make a great addition to POPL.
---------
- Well-coordination is an interesting criterion for correctness
- Impressive generality
- Automated and "correct-by-construction" approach
- The "multi-total-order broadcast" protocol seems useful and interesting on its own
-------------------------------------------------------------
CAV 20
-------------------------------------------------------------
- Principled design of replicated objects is a timely and important problem.
- The paper is very well written and a pleasure to read.
- The protocols are quite interesting and reveal new relationships
between various classes of guarantees. In particular, the interaction
between recency and convergence/integrity is an interesting issue,
which has not been discussed in previous work at this level of rigour.
- The idea of inferring staleness bounds for object state components is novel.
---------
The key insight seems to be the connection between quantified stale data, local buffer size, and performance.
Specifying staleness of the data is natural and the paper shows it is
also useful from a runtime perspective. In the context of eventual
consistency, method recency offers the programmer more control to
specify the low-level synchronization required, but in a light way, one
that saves the programmer from understanding all the formal definitions
of consistency.
...
I found novel and interesting the result that buffering pairs/tuples of
method calls that commute (w.r.t. each other) increases performance all
in preserving the required properties.
...
The connection with the fault-detector is also interesting.
---------
+ Expressive power of recency-aware objects captured precisely
+ The synthesized objects are heavily optimized to avoid unnecessary coordination at runtime
-------------------------------------------------------------
MAPL 20
-------------------------------------------------------------
This paper tackles a challenging problem - synthesizing an efficient
concurrent implementation from relational specification. ... Having an
ML model to predict the best decomposition for a given platform is a
natural and clean idea.
---------
This paper presents an elegant and useful approach to synthesizing
concurrent data structures, a notoriously difficult process. While the
author's technique obviously requires more work before it can be used
"in production," the research value of the work is clear and the
experimental analysis cleanly matches the claims of the paper, albeit
in a somewhat limited fashion.
-------------------------------------------------------------
ICFP 20
-------------------------------------------------------------
The paper represents the initial steps towards the large undertaking to
develop a formally verified distributed system middleware. Given the
complexity of the work, section 2 gives a great overview of the
technique and its applicability through the implementation and
verification of perfect links over stubborn links. I found the simpler
temporal logic specifications in Fig 3 to be quite pleasant and a
natural way to specify properties about distributed components. The
examples are tricky but the text makes it easy to follow. Specification
lowering as a method of composition is simple and elegant.
I also found the operational semantics to be novel in that it models
partially synchronous network and both the communication between
subcomponents at a particular node as well as communication between
nodes over base link which can drop, reorder and duplicate messages.
The typical operational semantics for distributed systems model the
network as asynchronous which makes them unsuitable for proving
consensus. Compared to the other works in this area where the proofs
are through refinements between layers modeled as transition systems, I
find TLC to be useful in lifting up the level of abstraction in proving
distributed system middleware.
--------
First of all, I should say that I am glad someone is pursuing this line
of research. It seems eminently worthwhile to investigate what it
takes to refactor previous specification and verification efforts in
distributed systems into a temporal component logic with sound
composition principles. At the outset, it is not at all clear
whether and how this might be accomplished. And at this point in
the larger research program there are some definitive successes: a
logic that is sound with respect to a plausible semantics has been
defined and applied to components that I would say have intermediate
complexity. One is always tempted to ask for more, of course,
especially since more complex distributed systems such as Raft have
already been verified, albeit in a different manner, as laid out by the
author. But I feel that the design of the logic and its illustration
has sufficient intrinsic merit and promise that it is worth publishing
to initiate discussion and to see where the future work might lead.
-------------------------------------------------------------
ICFP 21
-------------------------------------------------------------
This paper seems a real tour-de-force, representing a huge amount of
creative technical development, and a substantial amount of
engineering, and successful evaluation on real graphs.
-------------------------------------------------------------
S&P 21
-------------------------------------------------------------
I am impressed by the rigor of the paper; every concept and process is
formalized, and the system provides formal guarantees of
noninterference and resilience.
-------------------------------------------------------------
PODC 21
-------------------------------------------------------------
The problem is timely and well motivated, and the result appears clean.
-------------------------------------------------------------
|