1 00:00:00,000 --> 00:00:03,270 >> Hello, welcome to our presentation on 2 00:00:03,270 --> 00:00:06,915 TLA+ classification of PCR parallel programming pattern. 3 00:00:06,915 --> 00:00:08,519 This is a work in progress. 4 00:00:08,519 --> 00:00:12,300 My name is Sergio Yovine and I will be 5 00:00:12,300 --> 00:00:17,160 presenting this work together with Jose Solsona. 6 00:00:17,160 --> 00:00:21,345 We are both affiliated with Universidad ORT Uruguay. 7 00:00:21,345 --> 00:00:24,150 This is the agenda of our talk. 8 00:00:24,150 --> 00:00:33,360 We'll go through the main goals of our work and present the PCR, 9 00:00:33,360 --> 00:00:36,435 which is the parallel programming pattern. 10 00:00:36,435 --> 00:00:42,990 We are interested in modeling semantics in TLA+. 11 00:00:42,990 --> 00:00:49,800 I'll go through it with several examples and then Jose will take 12 00:00:49,800 --> 00:00:56,850 care of explaining briefly the TLA+ specification, 13 00:00:56,850 --> 00:02:16,350 and getting into the details of our work on that [inaudible] 14 00:02:16,350 --> 00:02:25,140 translators from PCRs into TLA+ to make this integration seamless. 15 00:02:25,140 --> 00:02:36,225 Let me first introduce the PCR; Produce-Consume-Reduce pattern. 16 00:02:36,225 --> 00:02:44,900 This is what we call parallel programming skeleton that actually 17 00:02:44,900 --> 00:02:50,930 encompasses several well-known programming skeleton 18 00:02:50,930 --> 00:02:54,140 such as MapReduce and others. 19 00:02:54,140 --> 00:03:03,605 The idea is that the component is made of 20 00:03:03,605 --> 00:03:08,090 a producer which can encompass one to 21 00:03:08,090 --> 00:03:12,710 many transformation that receives an input 22 00:03:12,710 --> 00:03:16,850 and produces a stream of data that are then 23 00:03:16,850 --> 00:03:21,905 consumed by a cascade of consumers. 24 00:03:21,905 --> 00:03:26,730 Each consumer itself is a one-to-one transformation, 25 00:03:26,730 --> 00:03:33,780 so it takes an input and outputs the same amount of data. 26 00:03:33,780 --> 00:03:39,135 At the end of this data flow graph, 27 00:03:39,135 --> 00:03:44,880 there is a reducer that is many-to-one transformation. 28 00:03:44,880 --> 00:03:52,425 It takes all data transformed by the producer and the consumers, 29 00:03:52,425 --> 00:03:56,250 and outputs as single value. 30 00:03:56,250 --> 00:04:03,105 Overall, a PCR is a one-to-one transformation. 31 00:04:03,105 --> 00:04:07,230 Basically, the data flow inside the PCR. 32 00:04:07,230 --> 00:04:09,135 It works out as we said. 33 00:04:09,135 --> 00:04:15,194 It produce and the producer generates a stream, 34 00:04:15,194 --> 00:04:17,900 and then the consumer reads 35 00:04:17,900 --> 00:04:20,405 the values, perform some transformation, 36 00:04:20,405 --> 00:04:23,780 outputs the value, and all values are then reduced 37 00:04:23,780 --> 00:04:28,055 to a single one by the producer. 38 00:04:28,055 --> 00:04:31,000 Some important remark is that 39 00:04:31,100 --> 00:04:39,090 all reads are non-destructive, 40 00:04:39,090 --> 00:04:46,445 so any produced value by the producer or the consumers are there, 41 00:04:46,445 --> 00:04:55,080 are not destroyed after read so they can be read multiple times. 42 00:04:56,840 --> 00:05:04,710 No data produced is ignored. 43 00:05:04,710 --> 00:05:12,580 So every item must be read at least once. 44 00:05:12,920 --> 00:05:16,440 Then all these components, 45 00:05:16,440 --> 00:05:18,375 producer, consumer, and reducers, 46 00:05:18,375 --> 00:05:22,970 inside the PCR work completely in parallel only restricted by 47 00:05:22,970 --> 00:05:28,770 the data dependencies between them. 48 00:05:28,940 --> 00:05:31,380 To be a little bit more concrete, 49 00:05:31,380 --> 00:05:37,280 we designed a language which basically has three components, 50 00:05:37,280 --> 00:05:41,570 which can be assignments 51 00:05:41,570 --> 00:05:46,540 to variables which are themselves strings. 52 00:05:46,850 --> 00:05:50,535 The producer has this syntax, 53 00:05:50,535 --> 00:05:56,370 p is equal to produce an x, 54 00:05:56,370 --> 00:05:59,630 where f is the basic function or 55 00:05:59,630 --> 00:06:07,325 another PCR which is in charge of producing the actual elements, 56 00:06:07,325 --> 00:06:12,105 and x is just the input to the PCR. 57 00:06:12,105 --> 00:06:17,260 So P is what we call an index variable, 58 00:06:17,900 --> 00:06:21,440 that this p represents the whole stream of 59 00:06:21,440 --> 00:06:24,440 data produced by the producer. 60 00:06:24,440 --> 00:06:27,155 Seq means that in some particular cases, 61 00:06:27,155 --> 00:06:32,365 the produce itself is a sequential process. 62 00:06:32,365 --> 00:06:37,640 Then the consumer is basically the same thing. 63 00:06:37,640 --> 00:06:40,310 It has some function 64 00:06:40,310 --> 00:06:43,250 f which is either a basic function or another PCR. 65 00:06:43,250 --> 00:06:49,515 The producer and consumers allow nesting of PCRs, 66 00:06:49,515 --> 00:06:54,945 that's the way PCRs are composed. 67 00:06:54,945 --> 00:06:59,250 The consumers take p, 68 00:06:59,250 --> 00:07:03,310 which is the produced variable and output. 69 00:07:03,680 --> 00:07:09,870 Data on c variable which represents the stream 70 00:07:09,870 --> 00:07:17,385 of variables generated by the consumers. 71 00:07:17,385 --> 00:07:21,060 Then there is a reducer, reduce, 72 00:07:21,060 --> 00:07:26,580 which basically applies a commutative and associative operation 73 00:07:26,580 --> 00:07:30,465 that has some initial neutral value, 74 00:07:30,465 --> 00:07:35,085 V_0, to the consumed 75 00:07:35,085 --> 00:07:37,950 or to the stream produced by 76 00:07:37,950 --> 00:07:42,280 the consumers to generate the final output of the PCR. 77 00:07:42,470 --> 00:07:46,320 We said we identify variables p, 78 00:07:46,320 --> 00:07:50,460 c describes the full history of assignments. 79 00:07:50,460 --> 00:07:56,100 Then to denote specific value, 80 00:07:56,100 --> 00:08:02,775 then we use sub indices of p_i is the i-th value produced, 81 00:08:02,775 --> 00:08:11,535 and c_i is the value produced by the consumers. 82 00:08:11,535 --> 00:08:20,445 Then the language allows for moving along the stream of data, 83 00:08:20,445 --> 00:08:22,530 performing either look-ahead or 84 00:08:22,530 --> 00:08:25,935 look-behind operations, for instance, 85 00:08:25,935 --> 00:08:33,374 if P_i is the i-th Fibonacci number produced by the producer, 86 00:08:33,374 --> 00:08:37,230 then in order to generate them, 87 00:08:37,230 --> 00:08:38,430 we can make use of 88 00:08:38,430 --> 00:08:44,460 the i minus 1 value and i minus 2 value to generate value of p_i, 89 00:08:44,460 --> 00:08:47,385 there's a look-behind operator. 90 00:08:47,385 --> 00:08:50,325 But we can also apply 91 00:08:50,325 --> 00:08:54,885 look-ahead operators moving forward on the string. 92 00:08:54,885 --> 00:08:56,835 In order to operate, 93 00:08:56,835 --> 00:09:04,545 the producer requires defining an iteration space, 94 00:09:04,545 --> 00:09:09,240 which is defined by the user. 95 00:09:09,240 --> 00:09:12,360 Then the iteration space is defined by a lower 96 00:09:12,360 --> 00:09:15,210 bound or an upper bound and 97 00:09:15,210 --> 00:09:21,045 a step function that defines 98 00:09:21,045 --> 00:09:28,570 all the indexes that need to be traversed during the computation. 99 00:09:28,700 --> 00:09:33,345 To illustrate the PCR concept 100 00:09:33,345 --> 00:09:39,029 through an example which is the count fibprimes, 101 00:09:39,029 --> 00:09:40,860 it's a process for counting the number 102 00:09:40,860 --> 00:09:46,955 of Fibonacci primes in an interval, 103 00:09:46,955 --> 00:09:51,740 we'll first present first version and 104 00:09:51,740 --> 00:10:00,170 then more refined version of it that involves composing PCRs. 105 00:10:00,170 --> 00:10:06,540 The first model is given by a producer 106 00:10:06,540 --> 00:10:13,140 that uses the Fibonacci function to produce Fibonacci numbers. 107 00:10:13,140 --> 00:10:19,590 Then consumers check primality 108 00:10:19,590 --> 00:10:24,030 on the Fibonacci numbers produced by the producer. 109 00:10:24,030 --> 00:10:29,985 Then reducer count basically counts 110 00:10:29,985 --> 00:10:38,339 all prime Fibonacci's generated by the consumers. 111 00:10:38,339 --> 00:10:45,705 On the left, we have the abstract syntax of PCR and on the right, 112 00:10:45,705 --> 00:10:48,390 we have its semantics. 113 00:10:48,390 --> 00:10:50,490 In the syntax, we have 114 00:10:50,490 --> 00:10:56,260 just the functions which are the basic functions. 115 00:10:56,330 --> 00:11:02,830 Fibonacci is prime and just the count. 116 00:11:02,900 --> 00:11:09,120 Then the user-defined iteration space, 117 00:11:09,120 --> 00:11:15,000 the lower bound and the upper bound and the step. 118 00:11:15,000 --> 00:11:21,195 In this case, x is going to be instantiated by 119 00:11:21,195 --> 00:11:29,670 the number of Fibonacci numbers that we want to generate. 120 00:11:29,670 --> 00:11:33,780 Then the iteration space is the set of index 121 00:11:33,780 --> 00:11:39,915 from 0-N. Then the Fibonacci primes, 122 00:11:39,915 --> 00:11:44,655 PCR, fibprimes1, has sequential producer 123 00:11:44,655 --> 00:11:47,085 go through the iteration space 124 00:11:47,085 --> 00:11:50,040 and then produce the Fibonacci numbers. 125 00:11:50,040 --> 00:11:57,975 Then we cover consumers that we check for primality, 126 00:11:57,975 --> 00:12:01,395 then the reduce that we count. 127 00:12:01,395 --> 00:12:04,455 The semantics is given by 128 00:12:04,455 --> 00:12:12,990 this direct acyclic graph of dependencies where p_0, p_i, etc. 129 00:12:12,990 --> 00:12:17,580 are the indexed values produced by the producer. 130 00:12:17,580 --> 00:12:21,645 Here it says that to produce value p_i, 131 00:12:21,645 --> 00:12:28,275 the producer needs p_i minus 1 and p_i minus 2. 132 00:12:28,275 --> 00:12:35,760 C_0 up to c_N are the values produced by the consumer, 133 00:12:35,760 --> 00:12:40,870 and we have a data dependency between c_0 and p_0, 134 00:12:41,000 --> 00:12:51,000 c_i with p_i, etc. 135 00:12:51,000 --> 00:12:53,985 The computation of all these c values, 136 00:12:53,985 --> 00:12:58,785 completely independent one on the other. 137 00:12:58,785 --> 00:13:02,700 It will be executed in any order. 138 00:13:02,700 --> 00:13:04,680 Then at the end, 139 00:13:04,680 --> 00:13:10,980 the reducer computes r, and to compute the r, 140 00:13:10,980 --> 00:13:13,305 it depends on all the values, 141 00:13:13,305 --> 00:13:16,395 then reducer can perform 142 00:13:16,395 --> 00:13:20,205 intermediate computations, and at the end, 143 00:13:20,205 --> 00:13:26,745 output the final output, 144 00:13:26,745 --> 00:13:31,245 which is the number of Fibonacci primes in this interval. 145 00:13:31,245 --> 00:13:37,470 This is the basic model specification of Fibonacci primes, 146 00:13:37,470 --> 00:13:41,280 but the function, isPrime, 147 00:13:41,280 --> 00:13:43,575 itself can also be paralyzed. 148 00:13:43,575 --> 00:13:45,330 We want to do that. 149 00:13:45,330 --> 00:13:51,750 In this case, we want to replace the function isPrime by PCR. 150 00:13:51,750 --> 00:13:57,405 In this case, when we resort to listing PCRs, 151 00:13:57,405 --> 00:14:02,530 we need to define 152 00:14:04,580 --> 00:14:09,570 an iteration space and the indexes of variables on 153 00:14:09,570 --> 00:14:17,350 a higher-dimensional space as list of indexes. 154 00:14:17,350 --> 00:14:21,900 We'll talk about the capital I is 155 00:14:21,900 --> 00:14:30,060 the iteration space of the upper level, 156 00:14:30,060 --> 00:14:34,880 and small i represent indexes in 157 00:14:34,880 --> 00:14:41,950 the iteration space which is local to the actual PCR. 158 00:14:41,950 --> 00:14:48,860 All variables in the execution of a PCR are indexed by 159 00:14:48,860 --> 00:14:53,090 a multi-dimensional space that will 160 00:14:53,090 --> 00:14:58,795 represent as a list or tuple of indexes. 161 00:14:58,795 --> 00:15:05,885 In this second version of the Fibonacci Prime counter, we expand, 162 00:15:05,885 --> 00:15:14,120 as I said before, the isPrime function here by PCR. Okay? 163 00:15:14,120 --> 00:15:22,075 Each time a consumer is executed, 164 00:15:22,075 --> 00:15:27,040 it will itself compute as 165 00:15:27,040 --> 00:15:33,025 a PCR where the producer is the one that produces the divisors, 166 00:15:33,025 --> 00:15:37,090 the consumers checks for where it divides or not. 167 00:15:37,090 --> 00:15:40,720 The user just makes the conjunction of 168 00:15:40,720 --> 00:15:44,680 all the outputs of the consumers. 169 00:15:44,680 --> 00:15:49,420 Basically this slide we have the same syntax 170 00:15:49,420 --> 00:15:54,640 as before where we expanded its prime as a PCR, 171 00:15:54,640 --> 00:15:59,950 which is here from lines 21-26 as exactly the same structure. 172 00:15:59,950 --> 00:16:06,654 Here we show the iteration space of the divisors, 173 00:16:06,654 --> 00:16:10,990 and on the right we see the same graph as before 174 00:16:10,990 --> 00:16:15,340 where we have added more notes here, 175 00:16:15,340 --> 00:16:24,800 which represents the data dependencies inside the isPrime PCR. 176 00:16:24,870 --> 00:16:30,700 The stand for the divisors which we see here that are 177 00:16:30,700 --> 00:16:37,180 indexed with couple of numbers, 178 00:16:37,180 --> 00:16:43,780 the first one corresponds to the index of the parent your C, 179 00:16:43,780 --> 00:16:48,160 and the second number corresponds to the local, 180 00:16:48,160 --> 00:16:53,590 either interspace in likes of the PCR, 181 00:16:53,590 --> 00:17:00,020 generated by the producer in the isPrime PCR. 182 00:17:00,060 --> 00:17:06,910 Essentially the same pattern of dependencies is 183 00:17:06,910 --> 00:17:13,780 shown as in the parent PCR. 184 00:17:13,780 --> 00:17:20,650 A represent the results 185 00:17:20,650 --> 00:17:27,950 of the reaction of the reducer in the isPrime PCR. 186 00:17:28,080 --> 00:17:33,160 >> Hello everyone. My name is Jose and I'm going to show you 187 00:17:33,160 --> 00:17:38,215 our TLA + specification of the PCR concepts we have seen earlier. 188 00:17:38,215 --> 00:17:39,835 First, I'm going to discuss 189 00:17:39,835 --> 00:17:42,200 the high level overview of our projects. 190 00:17:42,200 --> 00:17:44,370 We organize our projects across 191 00:17:44,370 --> 00:17:49,755 different TLA + modules in a way is convenient for us to handle. 192 00:17:49,755 --> 00:17:52,065 There is a PCR-based module. 193 00:17:52,065 --> 00:17:53,985 In this module we have 194 00:17:53,985 --> 00:17:59,920 the principle definitions that we can find in every PCR. 195 00:17:59,920 --> 00:18:04,645 There is also a PCR iteration-based module. 196 00:18:04,645 --> 00:18:07,255 In this module we define some of 197 00:18:07,255 --> 00:18:10,765 related concerns to the definition of iteration basis. 198 00:18:10,765 --> 00:18:15,655 Every concrete PCR has its own module, 199 00:18:15,655 --> 00:18:18,595 it's called PCR, followed by its name. 200 00:18:18,595 --> 00:18:21,369 In these PCRs modules, 201 00:18:21,369 --> 00:18:25,000 the principle actions PC and R corresponding 202 00:18:25,000 --> 00:18:28,750 to the producer consumer or reduction behavior are the final. 203 00:18:28,750 --> 00:18:32,860 The results from main PCR module for the root PCR, 204 00:18:32,860 --> 00:18:36,910 that's called main PCR followed by the name of the root PCR. 205 00:18:36,910 --> 00:18:41,530 There's also a type of module, in this module, 206 00:18:41,530 --> 00:18:46,210 we collect the basic data types that we expect to be in 207 00:18:46,210 --> 00:18:51,595 the all the PCR modules in the system. 208 00:18:51,595 --> 00:18:55,705 In a PCR, variables are streams indexed with 209 00:18:55,705 --> 00:18:58,360 multidimensional indexes which are 210 00:18:58,360 --> 00:19:01,870 automatically generated by the underlying runtime system. 211 00:19:01,870 --> 00:19:04,735 We formalize this by using 212 00:19:04,735 --> 00:19:07,795 the concept of contexts and context mappings. 213 00:19:07,795 --> 00:19:12,640 Let VarPType and VarCType be basic data types. 214 00:19:12,640 --> 00:19:15,775 For the producer and consumer variables, 215 00:19:15,775 --> 00:19:23,335 we define VarP and VarC as functions from natural to records. 216 00:19:23,335 --> 00:19:26,590 In these records, the field v denotes 217 00:19:26,590 --> 00:19:30,400 the value of the variable at some assignment. 218 00:19:30,400 --> 00:19:33,805 Under field r, 219 00:19:33,805 --> 00:19:37,615 is used to keep track the number of time it has been read. 220 00:19:37,615 --> 00:19:43,375 The value NULL means the assignment has not occurred so far. 221 00:19:43,375 --> 00:19:47,545 A context represent the PCR state at inner scope. 222 00:19:47,545 --> 00:19:50,440 These are the components of the contexts. 223 00:19:50,440 --> 00:19:52,690 In is the input variable, 224 00:19:52,690 --> 00:19:56,980 i_p is the current iteration index, 225 00:19:56,980 --> 00:20:01,120 v_p and v_c are the producer and consumer history. 226 00:20:01,120 --> 00:20:07,674 Ret is the reducer result and there's a ste component, 227 00:20:07,674 --> 00:20:12,130 one of the multiple three states for the PCR. 228 00:20:12,130 --> 00:20:16,255 Multidimensional indexes are modeled by sequences of Nat. 229 00:20:16,255 --> 00:20:20,710 A context mapping is a partial function from indexes to contexts. 230 00:20:20,710 --> 00:20:24,805 Any PCR have its own context mapping map. 231 00:20:24,805 --> 00:20:34,300 So map of capital I is the PCR contexts at some index capital I. 232 00:20:34,300 --> 00:20:36,610 For convenience, we give names to 233 00:20:36,610 --> 00:20:39,680 context elements as you'll see here. 234 00:20:40,050 --> 00:20:47,529 We use regard notation to denote the values at any index. 235 00:20:47,529 --> 00:20:53,065 We define to some useful predicates over output variables. 236 00:20:53,065 --> 00:20:55,405 Here we have written and read. 237 00:20:55,405 --> 00:20:58,345 Written holds through if 238 00:20:58,345 --> 00:21:01,765 a variable has been written at some index, 239 00:21:01,765 --> 00:21:03,940 and read holds through if 240 00:21:03,940 --> 00:21:07,975 some variable has been read at some index. 241 00:21:07,975 --> 00:21:11,440 Any PCR has associated an iteration space, 242 00:21:11,440 --> 00:21:15,175 we define the index generated by the PCR. 243 00:21:15,175 --> 00:21:18,430 For these, we define an iterator operator, 244 00:21:18,430 --> 00:21:23,200 which describes a range in terms of high-order operators step, 245 00:21:23,200 --> 00:21:25,645 lower bound and upper bound. 246 00:21:25,645 --> 00:21:28,930 These higher-order operators correspond to 247 00:21:28,930 --> 00:21:33,850 the PCR syntax element discussed earlier. 248 00:21:33,850 --> 00:21:36,910 Every concrete PCR module describe 249 00:21:36,910 --> 00:21:42,145 its initial conditions by means of operator init context. 250 00:21:42,145 --> 00:21:46,105 Init context define the initial context 251 00:21:46,105 --> 00:21:51,290 as a record with input value. 252 00:21:51,390 --> 00:21:56,660 An i_p set at the lower bound of the input x. 253 00:21:56,730 --> 00:22:04,675 V_p and v_c are initializer has not written yet. 254 00:22:04,675 --> 00:22:09,145 Ret is initialized as a neutral value, 255 00:22:09,145 --> 00:22:16,555 and the ste component is initialized as off. 256 00:22:16,555 --> 00:22:20,020 Every concrete PCR module also describe what is 257 00:22:20,020 --> 00:22:24,530 the possible next step as a disjunction of the actions. 258 00:22:24,870 --> 00:22:27,265 If a state is off, 259 00:22:27,265 --> 00:22:30,100 the only possible action is it to start. 260 00:22:30,100 --> 00:22:32,500 But if it is running, 261 00:22:32,500 --> 00:22:38,380 the next possible actions can be PCR or quit. 262 00:22:38,380 --> 00:22:43,360 Quit is a convenient action 263 00:22:43,360 --> 00:22:46,270 that immediately terminates execution 264 00:22:46,270 --> 00:22:48,415 if the iteration space is empty. 265 00:22:48,415 --> 00:22:50,980 The main PCR module instantiates 266 00:22:50,980 --> 00:22:54,700 the root PCR and any other PCR involved. 267 00:22:54,700 --> 00:22:57,880 Here, the main system specification is defined. 268 00:22:57,880 --> 00:23:00,610 For example, let PCR1 and PCR2 269 00:23:00,610 --> 00:23:03,820 be two instance of some PCR modules. 270 00:23:03,820 --> 00:23:07,660 Then the main module for PCR1, 271 00:23:07,660 --> 00:23:10,615 assuming PCR1 is the root PCR, 272 00:23:10,615 --> 00:23:14,455 will have the following form. 273 00:23:14,455 --> 00:23:18,535 We see the Init state predicate 274 00:23:18,535 --> 00:23:23,095 initializes the context mappings for each of the PCRs. 275 00:23:23,095 --> 00:23:28,780 The next step says that any of these two PCRs can do an action. 276 00:23:28,780 --> 00:23:30,460 Now, we further illustrate 277 00:23:30,460 --> 00:23:34,795 our specification using the PCR fibPrimes 1 example. 278 00:23:34,795 --> 00:23:37,960 At the left, we have the PCR syntax, 279 00:23:37,960 --> 00:23:39,430 and at the right, we have 280 00:23:39,430 --> 00:23:42,260 the corresponding TLA plus specification. 281 00:23:42,260 --> 00:23:49,080 Axiom P at some index always require the EP variable to 282 00:23:49,080 --> 00:23:57,655 be in the iterator and update the context mapping accordingly. 283 00:23:57,655 --> 00:24:01,900 PB at EP index is 284 00:24:01,900 --> 00:24:06,655 set to the value computed by the Baskin function p, 285 00:24:06,655 --> 00:24:10,030 and EP is updated to 286 00:24:10,030 --> 00:24:13,660 the next value according to the step function. 287 00:24:13,660 --> 00:24:16,465 For the consumer specification, 288 00:24:16,465 --> 00:24:20,095 we have C action. 289 00:24:20,095 --> 00:24:23,815 It non-deterministically choose aniof 290 00:24:23,815 --> 00:24:31,180 the iterator for which BP has been written and has not been read, 291 00:24:31,180 --> 00:24:34,855 and for which the corresponding BC has not been written. 292 00:24:34,855 --> 00:24:41,515 This updates the context mapping, marking BPS read, 293 00:24:41,515 --> 00:24:44,710 and updating the BC value 294 00:24:44,710 --> 00:24:49,340 with the value computed by the basic function is fine. 295 00:24:49,340 --> 00:24:52,065 For the reducer specification, 296 00:24:52,065 --> 00:24:54,645 we have error action. 297 00:24:54,645 --> 00:24:58,830 It non-deterministically choose anifrom 298 00:24:58,830 --> 00:25:05,345 the iterator for which BC has been written and has not been read, 299 00:25:05,345 --> 00:25:10,855 and it updates the current context accordingly. 300 00:25:10,855 --> 00:25:13,584 It sets the read components 301 00:25:13,584 --> 00:25:17,155 to the value computed by the basic function count, 302 00:25:17,155 --> 00:25:23,620 incremented the read count on the variable vc, 303 00:25:23,620 --> 00:25:31,600 and update the state component according to predicate cDone. 304 00:25:31,600 --> 00:25:34,195 The cDone predicate holds true if 305 00:25:34,195 --> 00:25:39,040 every consumer variable on index other than i has been read. 306 00:25:39,040 --> 00:25:43,790 Now, we are going to discuss PCR element with nesting. 307 00:25:43,890 --> 00:25:49,375 PCR fibPrime 2 uses PCR isPrime as a consumer. 308 00:25:49,375 --> 00:25:53,125 In this case, isPrime is not a basic function, 309 00:25:53,125 --> 00:25:55,210 it is another PCR. 310 00:25:55,210 --> 00:26:02,185 First we note that the producer at PCR isPrime sequential, 311 00:26:02,185 --> 00:26:05,425 so it's different from the early one. 312 00:26:05,425 --> 00:26:09,175 In this case, it non-deterministically choose 313 00:26:09,175 --> 00:26:14,170 an i from the iterator for which vp has not been written, 314 00:26:14,170 --> 00:26:17,230 and updates the context mapping, 315 00:26:17,230 --> 00:26:19,120 in this case, map3. 316 00:26:19,120 --> 00:26:24,655 Now, for the consumer specification of PCR fibPrime 2, 317 00:26:24,655 --> 00:26:28,255 we have that the consumer goal 318 00:26:28,255 --> 00:26:31,930 is splitted in two parts, call and ret. 319 00:26:31,930 --> 00:26:36,730 In the first part, the action call, 320 00:26:36,730 --> 00:26:39,775 an index i is not deterministically chosen from 321 00:26:39,775 --> 00:26:45,490 the iterator for which vp has been written, has not been read, 322 00:26:45,490 --> 00:26:49,135 so the current context mapping, in this case, 323 00:26:49,135 --> 00:26:54,145 map2, is updated marking BP as real, 324 00:26:54,145 --> 00:26:57,595 and the context mapping of 325 00:26:57,595 --> 00:27:01,390 a module isPrime is 326 00:27:01,390 --> 00:27:05,965 updated with the corresponding in each i context. 327 00:27:05,965 --> 00:27:12,490 For C_ret, an i is non- determinitically 328 00:27:12,490 --> 00:27:14,935 chose from the iterator 329 00:27:14,935 --> 00:27:16,990 for which we [inaudible] has been written 330 00:27:16,990 --> 00:27:18,895 and for which correspondingly, 331 00:27:18,895 --> 00:27:21,220 PC is not written, 332 00:27:21,220 --> 00:27:26,320 and for which isPrime has finished. 333 00:27:26,320 --> 00:27:30,385 Then map2 is correspondingly 334 00:27:30,385 --> 00:27:35,095 updated with the value computed by the instant isPrime, 335 00:27:35,095 --> 00:27:38,170 and this is set In vc. 336 00:27:38,170 --> 00:27:40,810 Correctness and termination properties 337 00:27:40,810 --> 00:27:43,240 are specified in the main module. 338 00:27:43,240 --> 00:27:45,774 Our two previous PCR examples, 339 00:27:45,774 --> 00:27:49,135 fibPrime1, fibPrime2, have the same properties. 340 00:27:49,135 --> 00:27:55,435 Solution is the expected behavior for these PCR. 341 00:27:55,435 --> 00:28:00,205 It computes all the fibonacci prime numbers 342 00:28:00,205 --> 00:28:04,060 in the interval from zero to some number x. 343 00:28:04,060 --> 00:28:08,350 So correctness is stated as forever if 344 00:28:08,350 --> 00:28:12,850 fibPrimes have finished then fibPrimes out, 345 00:28:12,850 --> 00:28:17,785 that is the output of the primes equals the solution on the 346 00:28:17,785 --> 00:28:23,530 variable N. N is the input variable of the specification. 347 00:28:23,530 --> 00:28:28,885 Termination is stated as eventually, fibPrime has finished. 348 00:28:28,885 --> 00:28:34,495 We assume the root PCR start at context zero. 349 00:28:34,495 --> 00:28:36,805 We can relate fibPrimes 1, 350 00:28:36,805 --> 00:28:39,610 fibPrimes 2 by proving the latter is 351 00:28:39,610 --> 00:28:40,660 an implementation of the 352 00:28:40,660 --> 00:28:44,080 former under an appropriate refinement mapping. 353 00:28:44,080 --> 00:28:47,755 In the main module of fibPrime 1, 354 00:28:47,755 --> 00:28:51,025 there is a concept mapping, map1. 355 00:28:51,025 --> 00:28:53,920 We consider these the high-level spec. 356 00:28:53,920 --> 00:28:56,815 In the main module of fibPrime 2, 357 00:28:56,815 --> 00:29:03,100 there are two context mappings namely map2 and map3. 358 00:29:03,100 --> 00:29:05,245 We consider these the low-level spec. 359 00:29:05,245 --> 00:29:10,210 In this module, we instantiate the main module of the fibPrime 1 360 00:29:10,210 --> 00:29:17,305 with map1 substitute for an expression in terms of map2 and map3. 361 00:29:17,305 --> 00:29:19,390 Here is the expression. 362 00:29:19,390 --> 00:29:21,684 This refinement work by contracting 363 00:29:21,684 --> 00:29:24,850 the time between the actions call and ret, 364 00:29:24,850 --> 00:29:27,700 to satisfy the behavior on 365 00:29:27,700 --> 00:29:30,580 the consumer action in the high-level spec. 366 00:29:30,580 --> 00:29:34,405 In this refine, we have to take care 367 00:29:34,405 --> 00:29:39,100 of variables vp and vc of the producer and consumer. 368 00:29:39,100 --> 00:29:40,735 In the case of vp, 369 00:29:40,735 --> 00:29:42,760 we have that for in assignment, 370 00:29:42,760 --> 00:29:49,480 we need to keep the fill r as zero, 371 00:29:49,480 --> 00:29:57,760 that is marked as not real until isPrime have finished it. 372 00:29:57,760 --> 00:30:02,470 In the case of vc, we have that for in assignment if 373 00:30:02,470 --> 00:30:05,830 the corresponding vp variable has been 374 00:30:05,830 --> 00:30:10,510 read and isPrime has finished it, 375 00:30:10,510 --> 00:30:15,415 then the v field 376 00:30:15,415 --> 00:30:19,870 has to be set with the output computed by the isPrime instance. 377 00:30:19,870 --> 00:30:23,575 Some remarks about model checking and theorem proving. 378 00:30:23,575 --> 00:30:26,890 We always try to make the specifications to 379 00:30:26,890 --> 00:30:30,460 be friendly with a model checker TLC, 380 00:30:30,460 --> 00:30:34,015 and the theorem prover, TLAPS. 381 00:30:34,015 --> 00:30:38,590 Currently, we can model check properties like correctness, 382 00:30:38,590 --> 00:30:43,330 termination, and refinements on at least small models. 383 00:30:43,330 --> 00:30:45,820 If it is possible or not, 384 00:30:45,820 --> 00:30:48,955 it depends heavily on the problem. 385 00:30:48,955 --> 00:30:51,340 For very large state space, 386 00:30:51,340 --> 00:30:53,395 simulations can be useful. 387 00:30:53,395 --> 00:30:55,090 Really, model checking is 388 00:30:55,090 --> 00:31:00,595 useful to make sure that our intuitions are correct. 389 00:31:00,595 --> 00:31:06,160 Currently, we have only used the TLAPS to prove type invariance, 390 00:31:06,160 --> 00:31:11,455 but we hope to prove correctness or refinement properties. 391 00:31:11,455 --> 00:31:13,915 We currently have applied 392 00:31:13,915 --> 00:31:18,295 the presented approach to other known problems like Count Words, 393 00:31:18,295 --> 00:31:24,835 MergeSort, and NQueens, but we are working in other examples also. 394 00:31:24,835 --> 00:31:30,520 We are missing some [inaudible] for the PCR syntax, 395 00:31:30,520 --> 00:31:33,860 iterate and feedback loop. 396 00:31:34,260 --> 00:31:39,490 We also are missing handle of early termination. 397 00:31:39,490 --> 00:31:46,410 We believe we can attempt a translation from PCR to the TLA plus, 398 00:31:46,410 --> 00:31:48,210 and we expect to formalize 399 00:31:48,210 --> 00:31:52,050 an abstract model of a target execution runtime, 400 00:31:52,050 --> 00:31:54,015 and to prove refinements. 401 00:31:54,015 --> 00:31:56,200 Thank you very much.