Discover[i]: Component-based Parameterized Reasoning for Distributed Applications

>>Hi, everyone. So I guess everybody here knows me, but I’m supposed to say this. So I’m Madan Musuvathi
from the Research in Software Engineering group and it’s my pleasure to introduce
Roopsha today. She’s an Assistant
Professor at Purdue and she’s doing lots of exciting work in the intersection
of formal methods, programming languages, and machine learning and
program synthesis. So Roopsha.>>Thanks, Madan. Thanks
for the invitation. I’m really happy to be here. This is actually my first
time at Microsoft Research, Redmond and it’s so
wonderful to be here. So before I talk about
the main topic of this talk which is our
new discovery project, I wanted to tell you
a little bit about some of the other things
that I work on with my students as well as with the broader group of my
wonderful colleagues at Purdue. So we are PurPL, Purdue’s Programming Languages
Group and we are a group of nine faculty across the
computer science and ECE departments along
with our students, working on a whole bunch of fairly
diverse and exciting projects, spanning software
engineering, formal methods, programming languages, and systems. So let me show you some
snapshots of some of the really brief snapshots of some of the other projects
that I had been working on. My overall research agenda has
always been to make it easier to write reliable programs using techniques based
on automated reasoning. So as Madan said, my background and
most of this work has been at the intersection
of formal methods and programming languages, and I focus primarily
on problems such as program repair and program
synthesis and always end up, of course, reasoning also
about program verification, and I’ve looked at a bunch
of different domains, concurrent systems, distributed
systems more recently, machine learning more recently, and also personalized education which has been something that
I’ve been looking at for a while. So as I said, I have been interested in automatic
program repair for some time, where given an incorrect program that does not satisfy
some specification. So here’s an incorrect
program and here is a specification and you don’t
really need to look at these. The goal is to modify the program
using some class of permissible edits so that you end up with a program that then
satisfies the specification. So typically, you do want to obtain a program that corresponds to some desirable fix to the
original program, right? You don’t want to end up with a
completely different program. You really want to capture
programmer intent. So you want to minimize the change that you’re doing
to the original program, and typically this
has been captured as minimizing the syntactic change that one does to the
original program. But well, you could do a small minimal syntactic change to a program and change its
semantics dramatically. So our main hypothesis in program repair has been to also
consider the change that one does to the semantics of the program through the use of what
we call semantic program distances when guiding
the search towards finding suitable repair and
we have validated this does enable us to find more
desirable fixes more often than not and also really help make the search space more tractable. So that’s cost of a program repair. Somewhat related project
that we have just completed is for program clustering for introductory
programming assignments. There, you essentially cluster similar programs in order to
drive instructional tasks, such as just examining
the solution analysis or feedback generation or repair
like on the previous slide. So the traditional techniques for program clustering
essentially rely on doing syntactic comparisons between programs such as
looking at the edit distance, created distance between the
abstract syntax trees and then using this expensive pairwise
analysis between programs to cluster
programs together. What ends up happening is that the
number of clusters generated is really large to be really useful
because small syntactic changes, again, just end up putting very similar programs
into different clusters. So our insight has been to take a program and
then transform it into a feature vector and then
use these feature vectors to essentially just do k-means clustering to end up
with the final clustering. So this solves two issues. One is, we avoid the expensive
pairwise program analysis, right? All we have to do is just compute the Euclidean distance between
program feature vectors. The second thing is that in computing
this program feature vector, we completely ignore the
syntax of the program and we do this by focusing on
purely semantic features. So it’s a combination
of two features, one of which captures the
control flow signature of the program and the other one captures the dataflow
signature of the program. So again, the other results
here are really good. The number of clusters
reduces dramatically from existing techniques,
but more interestingly, we have done a bunch of
ground-truth experiments where we know what solutions, what algorithm solutions
correspond to, and we have found that we are
able to cluster them exactly. So if you have algorithms
doing recursion versus iteration versus something
else and we know those labels, our clusters exactly correspond
to those algorithmic labels. Yes.>>Is a feature vector specific to the one program execution
or can you separate->>So I did not. Yes. It’s all right.>>Static from this dynamic?>>No. So this is a bunch
of execution traces.>>Okay.>>There is actually
a test suite that is used to generate a
bunch of executions.>>I see.>>We used those executions to essentially extract
this feature vector.>>Okay. So but it is dynamic.>>It is dynamic.>>If some trace doesn’t
go down a certain path, it won’t show up as part
of the feature vector.>>True.>>Okay.>>Yeah.>>But you said that you
distinguish between say algorithm.>>Algorithmic essence. Yeah.>>But the same function may be implemented using
different algorithms. So the same functions would be in different clusters using this method.>>By functions what do you mean?>>Suppose you have
sorting functions.>>Yeah. So we are
able to distinguish between different sorting algorithms.>>Okay.>>Yeah. If it’s used in a larger program and the
sorting algorithms default, they would be in different clusters.>>So whats the use of that one? So why would you?>>So why would we do this?>>Yeah.>>Well, because our
hypothesis is that for instructional tasks
where an instructor needs to analyze and
examine and grade, let’s say, 1,000 solutions, you want to identify the unique different solutions in terms of algorithms
that are there.>>So you assume that the
program solve the same problem?>>Yes.>>Within those who you want to find.>>These are all solutions to
the same programming assignment. Sorry if I didn’t make that clear. So here is another very new
project that’s related to program where we are trying to actually push the boundaries of how we can reason
about neural networks. So there have been now
several papers that do formal reasoning for neural
networks in terms of verifying properties of different
kinds of neural networks. So we want to step in when the
verification fails and then use some counterexample-guided
loop to do repair. So what does repair mean? We want to essentially
modify the parameters of the network so that it ends
up satisfying the property. So this is a challenging
problem and we are essentially experimenting with different ways
of combining symbolic reasoning, symbolic search with the gradient
descent-based optimization, but really we have a
long way to go here. So I just wanted to mention this. Here, similar to the case as was
the case with program repair, it’s really important to
include some notion of how much you’re changing the
neural network semantics, which is essentially encapsulated
in its accuracy or it’s faithfulness to the training dataset when you are modifying the
neural network parameters. So again, there is some
notion of distances between the original and the
modified neural networks. Here’s another fun interesting
project that targets essentially the ambiguity resolution or the generalizability problem of example-based synthesis
where as you-all know, examples are incomplete
specifications which are easy to provide and
make synthesis tractable. But then they have this
problem of being incomplete. So there are many programs that
could satisfy the examples, but do not really capture the
implicit programmer intent. Usually what is done is, one streamlines the hypothesis
space by placing some kinds of syntactic bias on
the hypothesis space through the use of
highly-structured DSS or sometimes through the use of ranking functions
that are designed for some specific domains that order the programs according
to their syntax. But even with all of this, it doesn’t solve the generalizability
problem and neither do we, but we present another
approach to address this. So here is a partial program that is written as an input to the
sketch program synthesizer. As you can see, this
already places a lot of syntactic bias on
the hypothesis space. It’s really specifying the
structure of the program. Here, what the user
is trying to do is use this partial program essentially to synthesize a program that
computes the max of three integers, and for this fairly innocuous
looking example set, sketch fails to synthesize
the right program. So our framework is essentially for augmenting
this example-based synthesis by placing a semantic bias on the hypothesis space using what we call relational
perturbation properties. An applicable property
for this program is permutation invariance which says that if you permute or
perturb the inputs, the output perturbation is zero, the output remains unchanged. So we can apply this
property to augment the original user-provided
example set to generate a much larger augmented example
set and then use sketch or whatever synthesizer we’re using with this larger example
set to the synthesis. We have shown that
this definitely helps improve the generalizability
of the synthesizer. Ultimately, we check
correctness because we have some offline complete
functional specifications for the programs and we
are able to check if the synthesizer synthesizes
the right program.>>So the trick was
to permute inputs?>>Yes, and leave the
outputs unchanged.>>So that would apply
to programs that work over permutations decisions. So max and sorted?>>Right.>>So is it biased
towards the [inaudible].>>Good question. So we have a parametric representation of
relational perturbation properties. These include structural
perturbations such as permuting the indices of arrays, matrices, and so on and examining the corresponding
permutation in the outputs. There are also value
perturbations where you might apply some affine
transformation to all the elements and examine the corresponding
affine transformation and the outputs, and so on. The question is, now what
would happen to programs that actually do not satisfy any of these relational
perturbation properties?>>Are the set of programs
that are used for evaluating synthesized
sketching, are they->>No, they are not.>>Due to the->>They are not restricted
to programs that satisfy such relational
perturbation properties. So we have shown that we only improve on the performance of sketch
over all benchmarks. So there are three different
user interaction scenarios for obtaining these applicable
relational perturbation properties. The user can provide them
or the user can be using some feedback loop to validate
some perturb examples and so on. But we have also a scenario where we automatically infer a subset of
properties that is applicable, and when we’re inferring
these properties, we include both the properties as well as their negation in the set. So even if we are
actually inferring that the negation of the property holds, we are still able to add some semantic bias to
the hypothesis space. So we mainly evaluated this with
the sketch synthesizer and with a bunch of benchmarks from
its repositories that were programs or a bit
vectors and integers. For bit vectors, the performance
improvement in some cases was close to 200 percent. So hopefully there is a
generalization of this. One needs to find applicable
perturbation properties in different domains so that
we can use these adversarial machine learning inspired
techniques to expand set of examples and bias the
search semantically. Finally, I’ll just briefly
mentioned this project. This is the most related to
what I am going to speak on. This is a project that I did during my postdoc of our inference
of synchronization such as locks and notify primitives for shared-memory concurrent programs such as Linux Device Drivers. Here, we essentially used a counterexample generalization
based synthesis or repair loop. In each iteration, we took
a counterexample and we generalized it to a set of
related counterexamples, and then use this to infer
the synchronization. There were two classes of
properties that we consider. So we can handle standards
safety properties, assertions, pre-conditions,
post-conditions, and so on. But we also did this for a generic property that
we found was suitable for this domain of Linux
Device Drivers that we call preemption-safety where
the verification problem was not a reachability problem. It ended up being a
language inclusion problem, and so we have to
address that as well. But that’s all I want
to say about this, I’m welcome to take
more questions later. I do want to start talking
now about Discovery, which was the main
topic of this talk. So this is work that I’m doing
with my students Nour Jaber, who I’d go supervised with
my Purdue colleague, Milind. Also with Swen Jacobs
from Saarland University, who was an expert on
parameterized verification. This week is the first
time I’m giving this talk. I also spoke about this at UW
[inaudible] two days back. But really, this is
very much ongoing work. So I welcome discussion and feedback. This talk is about
distributed systems, which as we all know span evermore increasing aspects of our
ever increasing digital lives. Obviously, these
distributed systems do not always behave as intended. What are really the challenges
in building distributed systems? There are many challenges, and I’m going to obviously enlist
the ones that we have handled. So distributed systems
are built on top of building blocks that
are fairly complex. So think of building blocks such as; Consensus Protocols, Atomic Commits, Reliable Broadcasts, what have you. So reasoning about higher
level functionality of a distributed system, entails reasoning about these
intricate building blocks which might, for instance, involve exchange of a whole bunch
of messages to do something simple like electing a leader from a set of
communicating processes. So we are unable to reason about higher
level functionality without digging deep into the details
of these building blocks. So that is one challenge
that we hope to address, and the complexity of really reasoning about
these building blocks, for instance, consensus, is
evident from the huge body of very nice increasingly
sophisticated approaches that have come up for verifying or reasoning
about consensus protocols, both using fully automated or semi-automated techniques,
also from MSR. So the second challenge is that, if we want to reason about these
systems in an automated fashion, then we have to think
of these systems as a family of distributed systems, each with a different
number of processes. So we have to be able to reason about systems with
an arbitrary number of processes which is essentially the parameterized
verification problem, which is a well-known
undecidable problem. So that’s a big bottleneck
that we have to tackle for automated reasoning. Of course, for all software systems, but particularly so far
distributed systems, these are highly susceptible
to programmer errors because of their deep complexity. So our Discovery project essentially seeks to address
these challenges through parameterized verification
and synthesis of distributed systems that are built
on top of verified components. So to make this more precise, we observe that for certain systems that are built
on top of some building blocks, it’s possible to cleanly isolate the behavior of the building blocks, the building block itself, and replace the building block with some abstraction along with some
guarantees about its behavior. This is, for instance, possible
in for consensus protocols, and I will expand on that
through the course of my talk. Once we have these abstractions, then this enables us to take
a step back and reason about the higher level functionality of the system that is built
around these abstractions, that is built around
these building blocks. So that is our ultimate goal. We do want to reason about parameterized verification
for these systems and do parameterized synthesis
for these systems to ensure correctness for an
arbitrary number of processes. So today’s talk is about discovery instantiated with consensus
protocols as building blocks. So let’s start by looking at
our abstraction for consensus. But before I present that to you, let me just show you
our basic system model. The animation seems to
be a little messed up. So our systems consists
of processes that are essentially identical
finite state machines. They are composed asynchronously using standard
interleaving semantics. So you as the global
state transition system, at any step, exactly one
process makes a step. Apart from these processes are synchronized using
communication actions. So we allow a broadcast
communication and rendezvous communication or
peer-to-peer communication. So for instance, there might be a sender process and one receiver process or
all receiver processes, whether you are doing
peer-to-peer or broadcast. Then all the involved processes, together, take a step
towards their next states. They simultaneously make
a transition to the next. This is a synchronized step. Apart from these, I haven’t
shown these on the slide, but the processes also
have local variables and guarded commands over
these local variables. So one thing I wanted to clarify are some of the strong assumptions
that we make in this work, there are no failures here. There was just a lot of complexity
to deal with right now. That is the next thing on our agenda, but we do not allow any failure, processes don’t fail,
channels are ideal. Message delivery is instantaneous. There are no message delays. There is no message reordering, and so on. Yes.>>Isn’t in [inaudible]>>Not yet. No, we
cannot handle that.>>Okay. So it’s [inaudible]>>Yeah. The kinds of properties that we are interested in
are LTL properties broadly. But as I’ll show you later, we have decidability only
for safety properties. We can’t handle lightness
properties yet. So that’s our basic system model. Now, let’s just take a
step back and examine what the essence of a
consensus protocol is. So what does a consensus
protocol essentially do? It enables a set of participating processes
here, let’s say processes 1, 2, and 4 to reach an
agreement on a set of values. The cardinality of the set is also an input to this
consensus protocol. As an output, you
get a set of values, or winning proposals, or
really processes, if you will. So we don’t really
distinguish between values, or proposals, or processes. Since we want to be blind to
the exact strategy that is used by the consensus protocol or its implementation that we
are using as a building block, if you don’t really know which
subset of winners will be chosen, so we have to really examine
all the possible subsets of winners that can be chosen
from these participants. So let me just make this a bit more concrete in the context of our
global state transition system. So here is the example that I showed you where the
participants or processes 1, 2, and 4, and the set of
the cardinalities too. So consents around of
consensus begins in a state where all the participants know
who to reach consensus with, which means all the
participants are in some local states stayed that indicates that they are
ready for consensus. So on this slide, I indicate that with this C state, so processes 1, 2, and 4 are in a local state which indicates
they’re ready for consensus. Process 3, whose a
non-participant in our example, is in a don’t-care local state. So that’s going around
the consensus begins. Now at this point, we can invoke
some crazy consensus protocol. But what do we get at the end
of the consensus protocol? Well, we end up in a
global state where each processes local state is
globally consistent with each other. We end up, for instance, in a state, in this
example where processes 1, 2 are winners, process 4 is a loser, that’s green and pink. Of course, process 3 stays
in some don’t-care state, and they all know that
this is the case. They know if they have won or lost, and this is globally consistent. So now what we can do is, well, we can encapsulate such a
consensus round by ignoring what is the details
of the implementation because we are going to assume
that this has been verified. So I really want to
keep emphasizing this, that it’s okay for me to assume that a consensus protocol
or implementation has been verified because of all
these wonderful work on verification of
consensus protocols. I want to build on top of that
and see what else we can do. So we are going to forget
about this and encapsulate the details of this
round of consensus using a primitive
and a specification.>>So you are assuming
that while [inaudible] participating the consensus that’s
isolated from other processes.>>Yes.>>For example, three
could have started initiate the consensus with
four while one [inaudible]>>Right. So there can be non-interfering
simultaneous consensuses. I mean, where the participants
don’t intersect, that is allowed. But we cannot have
intersecting participant sets.>>So you can’t verify that that’s
an assumption that you have to->>That is an assumption.>>[inaudible]>>So yeah, I can state it as an assumption. I’m just thinking about
if there is a way to see that ultimately four has to decide who it is going
to participate in a consensus with and that
results that non-determinism, and then you just have one consensus. Then you have really two non-interfering
consensus protocols. Yes.>>I don’t who said
while they’re here, you made the assumption
that underneath, their packets are not
clause, your order, and etc. If you are assuming that this
lower layer is verified, you don’t have to worry
about any of that.>>Yeah. It’s more an assumption about the higher level system
I’m building around this.>>Okay.>>Sure. This can be this
can handle faults and so on.>>So in addition to
the consensus protocol, these different entities may also
send each other messages, right? That part of layer
your talking about, here you’re making that
simplifying a sense for that layer regardless
of the correctness?>>Exactly. Thanks for the
question and the clarification. Okay. So the primitive that we use
to abstract a way consensus is something that we call
choose for choosing winners. It’s essentially a global transition
that I’ll show you shortly. It’s a global atomic transition, and the specification is essentially a precondition,
post-condition pair. This, it talks about what the consensus start state has to satisfy and what the consensus
end state has to satisfy. Okay. So as I just mentioned, this choose primitive is
global atomic transition. Note that this cannot be
deterministic as I already said. This actually has to be
non-deterministic because we do not know exactly what strategies being
used and who the winners are. So this primitive is essentially an atomic non-deterministic
transition. So what are these axioms, or what is the specification
that I was talking about? Well, the consistent
participants condition, I mean, we formalize it, but what it essentially
encapsulates is that all processes know who they
have to reach consensus with. So they have all participants
agree on who the participants are. That’s really what the
precondition means, and this post-condition,
let me just clarify this. For instance, if this is a state XC XC in the context of this
example this does not satisfy the consensus participants
condition because process one has really indicated that it is
interesting consensus but is not yet ready for consensus because it
has not yet reached its C state. So that doesn’t satisfy it. The consistent winners condition, the post condition
simply ensures that the local states of all processes are globally
consistent with each other. So that there is no doubt about who the winners are
and who the losers are. So that’s our abstraction. So this means that our basic system model that
I showed you earlier is now enhanced with these tools primitives combined with the specifications. So this is an extended model, and we now have to see if we can decide parameterized
verification for this model, which brings me to the
second bit about discovery. So parameterized verification
problem essentially asks, just to clarify, I think
everybody knows PMCP, but just to state it
a bit more formally, it asks if given a family of distributed systems
of the form m of n where essentially a
distributed system m of n consists of n
identical processes. It asks whether for the sum of distributed systems the
specification satisfied for each member of the family
if the specification is satisfied for all n. PMCP, as I mentioned already, is a well-known undecidable problem. There had been many
papers identifying various kinds of interesting
decidable fragments over the years. That mainly end up restricting either the communication model
or the network topology. For instance, sometimes the
processes are restricted to be organized in a ring or
the specification itself. There are two fragments
that I want to mention, well, obviously because our
results depend on them. So there is a Esparza et
al broadcast protocols, which essentially restricts the
communication to broadcasts. All processes communicate
with our processes. It’s a clique. The
topology is a clique, and the properties are
safety properties. There is another protocol
which is of interest to us which is Emerson and
Kahlon’s guarded protocols, where communication is done using certain classes
of global guards, not arbitrary global guards but either conjunctive global guards or disjunctive global guards
but not a combination. The topology is still a clique, and the properties are more general. There is also liveness. Okay. So this is
essentially LTL minus x. So it turns out that this extended model that we have that I’m going to just
refer to as the choose protocol, this is not subsumed by
any of these fragments. Surprise. It would have obviously have been
easier if that happened, but really this is a challenge that we have to tackle in
our vision for discovery. I mean, we can take a building
block and abstract it away, but then we end up with
a new system model for which doesn’t quite fit into any
of the known decidable fragments. We have to always make sure that
we design these abstractions carefully so that we can
somehow get decidability. So one of the key results
in our paper is that PMCP is decidable for
this extended model, for the choose protocol with
respect to safety properties. So I’m just going to show you some of the key steps that are
involved in this proof, each of which is an important
result in its own right. I won’t dive too deep, but I just want you to see
some of the key steps. So the first thing we do
is we define what we call, I mean the name
doesn’t really matter, but we call these guarded
broadcast protocols, which are higher level system
models than our choose protocols. We show that these higher
level system all of these guarded broadcast
protocols are decidable. Okay. So these are
actually an extension of Esparza’s protocols with
some global guards. So these combine the
Emerson Kahlon fragment and Esparza fragment in some way. Intuitively what these
correspond to are essentially partially synchronized round-based
distributed systems. That is, if you think about it, that is what you get when you have consensus because
consensus is a kind of synchronization point
where all the participants definitely synchronize
with each other, but also the non-participants
indicate that they are not interested in consensus. So these consensus essentially
establishes these rounds where you synchronize and then
move on to the next round where you might again possibly
have another consensus. So that is the
intuitive encapsulation of our higher level system model. Then we formalize this relation
between the higher level model, between guarded broadcast
protocols and choose protocols through
simulation equivalence, which allows us to say
that if for any n, if you had shown that
a higher level model here h just indicates
a high level model corresponding to the
guarded broadcast protocol, and the subscript l corresponds to the lower
level choose protocol. So this says that if
we have succeeded in ensuring correctness for
the higher level model, then we get correctness for the
lower level model and vice-versa. That’s all the simulation
equivalence is telling us, to formally show the correspondence
between these protocols, but that’s not it. To get the complete
decision procedure, we need what are cut-offs. So we derive cut-offs for PMCP for our higher level
guarded broadcast protocols, which essentially say that if
you have a verified correctness for distributed system at the higher level for the
cut-off number of processes, then you get parameterized
correctness. So stated differently if there is an error in a system
of an arbitrary size, then you will find that error
in a system that is of size c, where the number of
processes is c. Okay. That’s the property of a cut-off. So these are the three key points, the three key junctures in our proof, and let us see how we
can put all of this together to get decidability. It just concretizes what
I’ve been saying so far.>>[inaudible] for c?>>Yeah. We derive C for
certain classes of systems as a function essentially of the local
state space of the processes. I mean again, to give some intuition, the size of C can depend on how many processes can
be in an error state. This show that in the worst case, you might have to
track all the states. So it might be the number
of processes that can be in each possible state
of the state space. But of course, we focus on systems and properties
where this is small; for instance for mutual exclusion, to reach a state that
violates mutual exclusion, it’s enough to track
a system of size two. That’s the basic intuition. So basically we get these
cut-offs by analyzing how the model checking algorithm works
on the higher level model. Yes.>>So for broadcast variables, and not using cut outs.>>That decidability results is not. So that is why reduction prevents
structured transition systems. Which essentially, just builds off of Esparza’s proof as
well for his fragment.>>These are based on well
founded, a quasi model.>>Yeah.>>So there you don’t have it bound.>>No, there you don’t have a bound. So we are able to show
decidability for a larger class of protocols for which we
are done for the class of protocols for which we are
able to derive cut-offs, really. Yeah. You won’t have
cutoffs for all kinds of models where you might
still have decidability. Yeah you don’t always have
the small model property or even if you do have
a small model poverty, there are cases where it’s not useful because you
really have to track how many processes are in all
the states of the process. Oh, yeah. So that is why reduction to well-structured transition
system and I just want to mention that this
higher level protocol is essentially obtained through counter abstraction or on a predicate abstraction
over our choose protocol. So you are essentially
tracking for instance, how many processes are
in a particular state? That’s the counter abstraction. Then predicate abstraction
essentially helps you shrink the space based on what you’re
interested in tracking. So that’s the insight into what
went into proving each of these. As I was saying, I would like to just put
all of these together. So the cut-off essentially says that let’s try and verify
if the lower-level model, so a system in the
choose protocol with a cut-off number of processes
satisfies the specification. This is doable using model checking because this is
a finite state system. So once we have that what do we get? Because of the
simulation equivalence, we get that the higher-level model for same number of processes
satisfies the specification. Once we have that, based on the definition of cutoffs, we get parameterized correctness. We basically get correctness
for all systems, systems of arbitrary sizes
in the higher-level model. Again, using the
simulation equivalence, we are able to get correctness for all systems
in the lower-level model. Because that is what
we’re interested in. We are interested in PMCP
ultimately for choose protocols. But we had to go via these higher-level models because the choose protocols are still more complicated to reason about
directly. So that’s it. That’s the main parameterize
verification result and after that, the next part is relatively
straightforward, with just one loose
end that I mentioned. So parameterize synthesis, let me just contrast these
two problems a bit. So parameterized
verification takes in a specification and
a process template, a process finite-state machine. Then if it’s successful, you essentially get correctness
for systems of arbitrary size. Here, again, M of n is essentially
the asynchronous composition of these n identical
finite state machines. With parameterize synthesis, what you have is you have
the specification. But instead of a complete process, you have a skeleton of a process. A sketch of a process. In our case, essentially the state transition system with
missing guarded commands. But you can make this as
skeletal as you want. You’ll just have a
crazy or search space. The output of a successful
parameterize synthesis is a completed process template
that completes the holes, such that you get correctness for the distributed system obtained
by composing those templates.>>So you can’t leave the number of states as a random in your sketch?>>Not right now. But frankly, we should be able to
enforce some states but then you can add local
variables and states too. But it’s just going to be
completely incraftable.>>What’s the relationship between the small model C
and the number of states? Is it linear or is it exponential?>>No, it is linear.>>For the size of the state space.>>Or the size of the stat space.>>Process local state space. In the size of the number of
states in this process template.>>Which is the number of
states in the FSM, right?>>Yeah.>>Model or local variables.>>Yes. So but the
interesting cutoffs are ones that are as independent of
the value just for instance, mutual exclusion or a small-bounded
number of mutual exclusion. Because that becomes
again in incraftable.>>You’re going to show an example later on of the sketch like that?>>No.>>No. Just to see, so these are finite state
local processes but your load variables on
bounded? I’m just curious.>>Yes, it’s finite.>>[inaudible] small.>>Yeah, there are numerated types, and then there is essentially, a variable that indexes over
the processes, Booleans. So Booleans, enumerator types, and these process IDs. Let’s ignore what
happens when these fail. So there is already some cool work from [inaudible] group over
a few papers that does synthesis that essentially handles the core
synthesis problem for us. So if you have a distributed system with a fixed number of processes and your system model is
essentially the basic system model, then they are able to synthesize protocol completions for those kinds of systems for a fixed
number of processes. So this is just
counterexample-guided synthesis, where the synthesizer might
synthesize a completion or some guarded commands which
is checked by the verifier, some finite state model checker, which if it succeeds, we are done. If not, the synthesizer has a counterexample that it also has to include when
coming up with the synthesis. So the verifier, let me emphasize, heavily relies on
symmetry reductions, exploiting the fact that all the processes are
identicals for tractability, and the synthesizer is essentially
based on SMT and SyGuS solvers. So the SMT solver will give a table of interpretations mapping
the inputs to the outputs, and then the SyGuS solver, or the Syntax-Guided
Synthesis solver, will take this table
and then synthesize a symbolic expression
that satisfies the table. So this is what they have. What they do not have is of course
our extended choose protocol. So there is something
we had to do for that, and they don’t have
parameterized correctness. To get parameterized correctness, since we have cut-offs, the step is trivial. So we just instantiate this with a cut-off number of processes and we get parameterized correctness. So that’s easy. To be able to exploit the symmetry
reductions in this verifier, we had to also show that the choose protocol also permits these kinds of
symmetry reductions. That is something we had to show. That’s another property our
abstractions have to meet. Then here is a loose end that we haven’t worked on yet but we
are going to work on soon, which is the synthesizer cannot just generate an arbitrary
symbolic expression for these guarded commands. The symbolic expression
has to be parameterized. It really has to correspond to something that gives
us parameterized correctness. Because if you don’t
ask it to do that, then it’s just going to
synthesize a completion that works for the cut-off
number of processes, and that may not generalize. So we need it to generalize. So we really have to go back and look at our simulation
equivalents and cut-offs and make sure that we
are staying in this fragment. Ideally, we would like some syntactic constraints that
we can supply to the synthesizer, that essentially give us the
generalizability that we want. But this is something we
are working on right now.>>Different completions might have different C [inaudible] , right, or?>>No. So because
these properties are fixed and the essential
state transition system is fixed, we have C.>>C is independent of the
guards, is what you’re saying.>>Yeah. So I don’t really want to harp about this right now because this is
very much ongoing work. I have a table there because I
want to tell you we have a tool, we have an implementation. We have some case studies. We are currently working on cache coherence protocol
and a key-value store. What we have are some handmade
examples of sensor networks that are smoke detectors with biggest kinds of mutual
exclusion properties. We have a distributed
file system built on top of Google’s Chubby lock service, and we have this small aircraft
traffic control system with a bunch of different kinds
of mutual exclusion that talk about planes sharing
runways and so on. So as you can see, the number of cut-offs
that we had for these systems were fairly small, and hence the whole thing
was manageable. Yes.>>The local variables
are Boolean variables? [inaudible] Sorry.>>No. They can include these
enumerator types as well. But you’re right, one to
clarify what the domains are, how many variables that
are of what domain.>>So these are if and only
if that you showed earlier. So what if the synthesis fails? So this proves that it
doesn’t exist basically, [inaudible] of that template
that can implement this->>Property.>>Right.>>Yes, that’s right.>>So in these examples, you were using sketching
or the [inaudible].>>So these are synthesis examples.>>Synthesis, right.>>Yeah. These are
synthesis examples, yes.>>So then it depends on what the sketch [inaudible]
how the distribution->>So essentially, we
are trying to synthesize guarded commands over
these number of variables, where the number of
locations or states, think of the basic model, is given by this number. So this defines the SAT space.>>So it’s very open-ended sketch, where you could think of
a very constrained sketch saying the only thing
that changes zero to one.>>No. Yeah. No, we’re a
little better than that. So that’s pretty much what I
wanted to say about Discover[i]. Our long-term vision is of course to extend this to many other
different kinds of components, but we have to be careful about
how we design these abstractions for each of these components
to ensure decidability, cut-offs, symmetry, and so on. We definitely want
to tackle failures, really, as soon as we
complete this project. Then we would ideally like to
be able to handle liveness. We want to see if we can tackle that at least in some restricted cases. That’s it. Yes.>>Also, in this
context, in addition, this list there you find that
optimality in the sense that, when you have this
distributed protocol it’s expensive to send
messages around, etc. So it’ll be interesting to see if you can prove that, for instance, you need some specific structure, etc., to achieve, implement it. Yeah, [inaudible] implement the
specification; is that right?>>No. Sure, in any
synthesis repair question, some kind of optimality
criterion always makes sense. Of course makes the problem harder, but definitely, I’ll put
that on my list next time.>>But I think you can
trial and error. So you start with a specific template. For instance, you could
limit the number of perhaps->>You could do this in
a bounded way, sure. You bound the number of parameters
and that will increase. Sure.>>So for the [inaudible] team [inaudible]. I believe the main tools
that they could apply or applied to the [inaudible]
systems were that essentially, you had a culture of abstraction of the number of processes
and given states, and then each protocol
had a set of phases, and each phase you could
accelerate through phases and then you got to the
[inaudible] system, and then the well-quasi ordering. So in your case, if I understood it, you don’t depend on the
cut-off results. Is that tied->>Which part of our system doesn’t
depend on the cut-off results? Overall, we ultimately
get a decision procedure.>>Well, the main
trick, the main method that you use is reduction [inaudible] or systems that meet the
finite cut-off quality.>>No, but we get decidability of our guarded broadcast protocols from the well-quasi
ordering. Very neat.>>Any more questions?

3 thoughts on “Discover[i]: Component-based Parameterized Reasoning for Distributed Applications

  1. Look at parameter reasoning, using quantum computers, as the step up & set up drawn from class reasoning by category processing via algorithmic ordering.

Leave a Reply

Your email address will not be published. Required fields are marked *