>> Hello, welcome to our presentation on
TLA+ classification of PCR parallel programming pattern.
This is a work in progress.
My name is Sergio Yovine and I will be
presenting this work together with Jose Solsona.
We are both affiliated with Universidad ORT Uruguay.
This is the agenda of our talk.
We'll go through the main goals of our work and present the PCR,
which is the parallel programming pattern.
We are interested in modeling semantics in TLA+.
I'll go through it with several examples and then Jose will take
care of explaining briefly the TLA+ specification,
and getting into the details of our work on that [inaudible]
translators from PCRs into TLA+ to make this integration seamless.
Let me first introduce the PCR; Produce-Consume-Reduce pattern.
This is what we call parallel programming skeleton that actually
encompasses several well-known programming skeleton
such as MapReduce and others.
The idea is that the component is made of
a producer which can encompass one to
many transformation that receives an input
and produces a stream of data that are then
consumed by a cascade of consumers.
Each consumer itself is a one-to-one transformation,
so it takes an input and outputs the same amount of data.
At the end of this data flow graph,
there is a reducer that is many-to-one transformation.
It takes all data transformed by the producer and the consumers,
and outputs as single value.
Overall, a PCR is a one-to-one transformation.
Basically, the data flow inside the PCR.
It works out as we said.
It produce and the producer generates a stream,
and then the consumer reads
the values, perform some transformation,
outputs the value, and all values are then reduced
to a single one by the producer.
Some important remark is that
all reads are non-destructive,
so any produced value by the producer or the consumers are there,
are not destroyed after read so they can be read multiple times.
No data produced is ignored.
So every item must be read at least once.
Then all these components,
producer, consumer, and reducers,
inside the PCR work completely in parallel only restricted by
the data dependencies between them.
To be a little bit more concrete,
we designed a language which basically has three components,
which can be assignments
to variables which are themselves strings.
The producer has this syntax,
p is equal to produce an x,
where f is the basic function or
another PCR which is in charge of producing the actual elements,
and x is just the input to the PCR.
So P is what we call an index variable,
that this p represents the whole stream of
data produced by the producer.
Seq means that in some particular cases,
the produce itself is a sequential process.
Then the consumer is basically the same thing.
It has some function
f which is either a basic function or another PCR.
The producer and consumers allow nesting of PCRs,
that's the way PCRs are composed.
The consumers take p,
which is the produced variable and output.
Data on c variable which represents the stream
of variables generated by the consumers.
Then there is a reducer, reduce,
which basically applies a commutative and associative operation
that has some initial neutral value,
V_0, to the consumed
or to the stream produced by
the consumers to generate the final output of the PCR.
We said we identify variables p,
c describes the full history of assignments.
Then to denote specific value,
then we use sub indices of p_i is the i-th value produced,
and c_i is the value produced by the consumers.
Then the language allows for moving along the stream of data,
performing either look-ahead or
look-behind operations, for instance,
if P_i is the i-th Fibonacci number produced by the producer,
then in order to generate them,
we can make use of
the i minus 1 value and i minus 2 value to generate value of p_i,
there's a look-behind operator.
But we can also apply
look-ahead operators moving forward on the string.
In order to operate,
the producer requires defining an iteration space,
which is defined by the user.
Then the iteration space is defined by a lower
bound or an upper bound and
a step function that defines
all the indexes that need to be traversed during the computation.
To illustrate the PCR concept
through an example which is the count fibprimes,
it's a process for counting the number
of Fibonacci primes in an interval,
we'll first present first version and
then more refined version of it that involves composing PCRs.
The first model is given by a producer
that uses the Fibonacci function to produce Fibonacci numbers.
Then consumers check primality
on the Fibonacci numbers produced by the producer.
Then reducer count basically counts
all prime Fibonacci's generated by the consumers.
On the left, we have the abstract syntax of PCR and on the right,
we have its semantics.
In the syntax, we have
just the functions which are the basic functions.
Fibonacci is prime and just the count.
Then the user-defined iteration space,
the lower bound and the upper bound and the step.
In this case, x is going to be instantiated by
the number of Fibonacci numbers that we want to generate.
Then the iteration space is the set of index
from 0-N. Then the Fibonacci primes,
PCR, fibprimes1, has sequential producer
go through the iteration space
and then produce the Fibonacci numbers.
Then we cover consumers that we check for primality,
then the reduce that we count.
The semantics is given by
this direct acyclic graph of dependencies where p_0, p_i, etc.
are the indexed values produced by the producer.
Here it says that to produce value p_i,
the producer needs p_i minus 1 and p_i minus 2.
C_0 up to c_N are the values produced by the consumer,
and we have a data dependency between c_0 and p_0,
c_i with p_i, etc.
The computation of all these c values,
completely independent one on the other.
It will be executed in any order.
Then at the end,
the reducer computes r, and to compute the r,
it depends on all the values,
then reducer can perform
intermediate computations, and at the end,
output the final output,
which is the number of Fibonacci primes in this interval.
This is the basic model specification of Fibonacci primes,
but the function, isPrime,
itself can also be paralyzed.
We want to do that.
In this case, we want to replace the function isPrime by PCR.
In this case, when we resort to listing PCRs,
we need to define
an iteration space and the indexes of variables on
a higher-dimensional space as list of indexes.
We'll talk about the capital I is
the iteration space of the upper level,
and small i represent indexes in
the iteration space which is local to the actual PCR.
All variables in the execution of a PCR are indexed by
a multi-dimensional space that will
represent as a list or tuple of indexes.
In this second version of the Fibonacci Prime counter, we expand,
as I said before, the isPrime function here by PCR. Okay?
Each time a consumer is executed,
it will itself compute as
a PCR where the producer is the one that produces the divisors,
the consumers checks for where it divides or not.
The user just makes the conjunction of
all the outputs of the consumers.
Basically this slide we have the same syntax
as before where we expanded its prime as a PCR,
which is here from lines 21-26 as exactly the same structure.
Here we show the iteration space of the divisors,
and on the right we see the same graph as before
where we have added more notes here,
which represents the data dependencies inside the isPrime PCR.
The stand for the divisors which we see here that are
indexed with couple of numbers,
the first one corresponds to the index of the parent your C,
and the second number corresponds to the local,
either interspace in likes of the PCR,
generated by the producer in the isPrime PCR.
Essentially the same pattern of dependencies is
shown as in the parent PCR.
A represent the results
of the reaction of the reducer in the isPrime PCR.
>> Hello everyone. My name is Jose and I'm going to show you
our TLA + specification of the PCR concepts we have seen earlier.
First, I'm going to discuss
the high level overview of our projects.
We organize our projects across
different TLA + modules in a way is convenient for us to handle.
There is a PCR-based module.
In this module we have
the principle definitions that we can find in every PCR.
There is also a PCR iteration-based module.
In this module we define some of
related concerns to the definition of iteration basis.
Every concrete PCR has its own module,
it's called PCR, followed by its name.
In these PCRs modules,
the principle actions PC and R corresponding
to the producer consumer or reduction behavior are the final.
The results from main PCR module for the root PCR,
that's called main PCR followed by the name of the root PCR.
There's also a type of module, in this module,
we collect the basic data types that we expect to be in
the all the PCR modules in the system.
In a PCR, variables are streams indexed with
multidimensional indexes which are
automatically generated by the underlying runtime system.
We formalize this by using
the concept of contexts and context mappings.
Let VarPType and VarCType be basic data types.
For the producer and consumer variables,
we define VarP and VarC as functions from natural to records.
In these records, the field v denotes
the value of the variable at some assignment.
Under field r,
is used to keep track the number of time it has been read.
The value NULL means the assignment has not occurred so far.
A context represent the PCR state at inner scope.
These are the components of the contexts.
In is the input variable,
i_p is the current iteration index,
v_p and v_c are the producer and consumer history.
Ret is the reducer result and there's a ste component,
one of the multiple three states for the PCR.
Multidimensional indexes are modeled by sequences of Nat.
A context mapping is a partial function from indexes to contexts.
Any PCR have its own context mapping map.
So map of capital I is the PCR contexts at some index capital I.
For convenience, we give names to
context elements as you'll see here.
We use regard notation to denote the values at any index.
We define to some useful predicates over output variables.
Here we have written and read.
Written holds through if
a variable has been written at some index,
and read holds through if
some variable has been read at some index.
Any PCR has associated an iteration space,
we define the index generated by the PCR.
For these, we define an iterator operator,
which describes a range in terms of high-order operators step,
lower bound and upper bound.
These higher-order operators correspond to
the PCR syntax element discussed earlier.
Every concrete PCR module describe
its initial conditions by means of operator init context.
Init context define the initial context
as a record with input value.
An i_p set at the lower bound of the input x.
V_p and v_c are initializer has not written yet.
Ret is initialized as a neutral value,
and the ste component is initialized as off.
Every concrete PCR module also describe what is
the possible next step as a disjunction of the actions.
If a state is off,
the only possible action is it to start.
But if it is running,
the next possible actions can be PCR or quit.
Quit is a convenient action
that immediately terminates execution
if the iteration space is empty.
The main PCR module instantiates
the root PCR and any other PCR involved.
Here, the main system specification is defined.
For example, let PCR1 and PCR2
be two instance of some PCR modules.
Then the main module for PCR1,
assuming PCR1 is the root PCR,
will have the following form.
We see the Init state predicate
initializes the context mappings for each of the PCRs.
The next step says that any of these two PCRs can do an action.
Now, we further illustrate
our specification using the PCR fibPrimes 1 example.
At the left, we have the PCR syntax,
and at the right, we have
the corresponding TLA plus specification.
Axiom P at some index always require the EP variable to
be in the iterator and update the context mapping accordingly.
PB at EP index is
set to the value computed by the Baskin function p,
and EP is updated to
the next value according to the step function.
For the consumer specification,
we have C action.
It non-deterministically choose aniof
the iterator for which BP has been written and has not been read,
and for which the corresponding BC has not been written.
This updates the context mapping, marking BPS read,
and updating the BC value
with the value computed by the basic function is fine.
For the reducer specification,
we have error action.
It non-deterministically choose anifrom
the iterator for which BC has been written and has not been read,
and it updates the current context accordingly.
It sets the read components
to the value computed by the basic function count,
incremented the read count on the variable vc,
and update the state component according to predicate cDone.
The cDone predicate holds true if
every consumer variable on index other than i has been read.
Now, we are going to discuss PCR element with nesting.
PCR fibPrime 2 uses PCR isPrime as a consumer.
In this case, isPrime is not a basic function,
it is another PCR.
First we note that the producer at PCR isPrime sequential,
so it's different from the early one.
In this case, it non-deterministically choose
an i from the iterator for which vp has not been written,
and updates the context mapping,
in this case, map3.
Now, for the consumer specification of PCR fibPrime 2,
we have that the consumer goal
is splitted in two parts, call and ret.
In the first part, the action call,
an index i is not deterministically chosen from
the iterator for which vp has been written, has not been read,
so the current context mapping, in this case,
map2, is updated marking BP as real,
and the context mapping of
a module isPrime is
updated with the corresponding in each i context.
For C_ret, an i is non- determinitically
chose from the iterator
for which we [inaudible] has been written
and for which correspondingly,
PC is not written,
and for which isPrime has finished.
Then map2 is correspondingly
updated with the value computed by the instant isPrime,
and this is set In vc.
Correctness and termination properties
are specified in the main module.
Our two previous PCR examples,
fibPrime1, fibPrime2, have the same properties.
Solution is the expected behavior for these PCR.
It computes all the fibonacci prime numbers
in the interval from zero to some number x.
So correctness is stated as forever if
fibPrimes have finished then fibPrimes out,
that is the output of the primes equals the solution on the
variable N. N is the input variable of the specification.
Termination is stated as eventually, fibPrime has finished.
We assume the root PCR start at context zero.
We can relate fibPrimes 1,
fibPrimes 2 by proving the latter is
an implementation of the
former under an appropriate refinement mapping.
In the main module of fibPrime 1,
there is a concept mapping, map1.
We consider these the high-level spec.
In the main module of fibPrime 2,
there are two context mappings namely map2 and map3.
We consider these the low-level spec.
In this module, we instantiate the main module of the fibPrime 1
with map1 substitute for an expression in terms of map2 and map3.
Here is the expression.
This refinement work by contracting
the time between the actions call and ret,
to satisfy the behavior on
the consumer action in the high-level spec.
In this refine, we have to take care
of variables vp and vc of the producer and consumer.
In the case of vp,
we have that for in assignment,
we need to keep the fill r as zero,
that is marked as not real until isPrime have finished it.
In the case of vc, we have that for in assignment if
the corresponding vp variable has been
read and isPrime has finished it,
then the v field
has to be set with the output computed by the isPrime instance.
Some remarks about model checking and theorem proving.
We always try to make the specifications to
be friendly with a model checker TLC,
and the theorem prover, TLAPS.
Currently, we can model check properties like correctness,
termination, and refinements on at least small models.
If it is possible or not,
it depends heavily on the problem.
For very large state space,
simulations can be useful.
Really, model checking is
useful to make sure that our intuitions are correct.
Currently, we have only used the TLAPS to prove type invariance,
but we hope to prove correctness or refinement properties.
We currently have applied
the presented approach to other known problems like Count Words,
MergeSort, and NQueens, but we are working in other examples also.
We are missing some [inaudible] for the PCR syntax,
iterate and feedback loop.
We also are missing handle of early termination.
We believe we can attempt a translation from PCR to the TLA plus,
and we expect to formalize
an abstract model of a target execution runtime,
and to prove refinements.
Thank you very much.