>>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?

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

Thx!

thanks