1 00:00:00,530 --> 00:00:04,095 >> Hello. My name is Ron Pressler. 2 00:00:04,095 --> 00:00:07,605 By day, I work at Oracle and OpenJDK. 3 00:00:07,605 --> 00:00:10,470 That's the main implementation of the Java platform. 4 00:00:10,470 --> 00:00:12,990 But I've been working with TLA plus both 5 00:00:12,990 --> 00:00:16,605 professionally and mostly as a hobby for several years. 6 00:00:16,605 --> 00:00:21,760 This talk is intended is what I'll call a TLA plus Truffle. 7 00:00:21,890 --> 00:00:23,970 Back in the '80s, 8 00:00:23,970 --> 00:00:26,040 the computer scientist, Jon Bentley, 9 00:00:26,040 --> 00:00:27,990 wrote a column in the Communications of 10 00:00:27,990 --> 00:00:30,465 the ACM called Programming Pearls. 11 00:00:30,465 --> 00:00:31,845 That way she wrote, 12 00:00:31,845 --> 00:00:34,110 ''Just as natural pearls grow from 13 00:00:34,110 --> 00:00:37,020 grains of sand that has irritated oysters, 14 00:00:37,020 --> 00:00:39,060 these programming pearls have grown from 15 00:00:39,060 --> 00:00:42,025 real problems that have irritated programmers. 16 00:00:42,025 --> 00:00:43,760 The programs are fun, 17 00:00:43,760 --> 00:00:46,025 and they teach important programming techniques 18 00:00:46,025 --> 00:00:48,990 and fundamental design principles.'' 19 00:00:49,490 --> 00:00:52,545 Years later, Richard Bird 20 00:00:52,545 --> 00:00:55,250 edited a column in the similar vein in the Journal of 21 00:00:55,250 --> 00:00:58,160 Functional Programming and explained that a pearl is not 22 00:00:58,160 --> 00:01:01,205 original research or an industrial case study, 23 00:01:01,205 --> 00:01:04,745 but an instructive example, a nifty presentation, 24 00:01:04,745 --> 00:01:06,440 or an interesting application of 25 00:01:06,440 --> 00:01:08,930 a technique that should be polished, 26 00:01:08,930 --> 00:01:11,360 elegant, instructive, and entertaining. 27 00:01:11,360 --> 00:01:13,880 The idea was borrowed elsewhere in 28 00:01:13,880 --> 00:01:17,525 the form of graphics gems and perhaps others. 29 00:01:17,525 --> 00:01:19,460 In the same spirit, 30 00:01:19,460 --> 00:01:21,980 I'd propose TLA plus Truffles. 31 00:01:21,980 --> 00:01:24,995 I don't promise to live up to those standards, 32 00:01:24,995 --> 00:01:27,800 but I will try to offer something for everyone. 33 00:01:27,800 --> 00:01:30,245 Some manipulation of formal logic, 34 00:01:30,245 --> 00:01:32,435 some exploration of semantics, 35 00:01:32,435 --> 00:01:33,875 some use of TLC, 36 00:01:33,875 --> 00:01:36,140 and some interesting applications. 37 00:01:36,140 --> 00:01:40,260 We have quite a journey ahead of us so let's begin. 38 00:01:44,300 --> 00:01:47,715 As we all know, Leslie Lamport, 39 00:01:47,715 --> 00:01:50,995 the inventor of TLA plus and the logic as its core. 40 00:01:50,995 --> 00:01:53,785 The temporal logic of actions, or TLA, 41 00:01:53,785 --> 00:01:56,290 recommends that system specifications 42 00:01:56,290 --> 00:01:58,045 be written as state machines, 43 00:01:58,045 --> 00:02:00,550 which in TLA are written as 44 00:02:00,550 --> 00:02:02,380 the canonical formula of 45 00:02:02,380 --> 00:02:05,655 an initial states predicate, a state transition, 46 00:02:05,655 --> 00:02:09,955 or an action with a subscript that can be any state function, 47 00:02:09,955 --> 00:02:11,620 but normally is a tuple containing 48 00:02:11,620 --> 00:02:13,725 the variables mentioned in the formula, 49 00:02:13,725 --> 00:02:16,080 and some fairness conditions. 50 00:02:16,080 --> 00:02:18,270 This is very good advice. 51 00:02:18,270 --> 00:02:22,300 Indeed, the TLC model checker that comes with the TLA plus 52 00:02:22,300 --> 00:02:27,565 toolbox can only change TLA plus formulas of this canonical form. 53 00:02:27,565 --> 00:02:30,880 But I would like to talk about a different shape of formula. 54 00:02:30,880 --> 00:02:32,470 Show how it can be checked with 55 00:02:32,470 --> 00:02:35,745 TLC albeit with some inconveniences, 56 00:02:35,745 --> 00:02:40,860 and present three examples where such formulas could be useful. 57 00:02:41,680 --> 00:02:47,090 A TLA formula F specifies a class of behaviors, 58 00:02:47,090 --> 00:02:49,390 where a behavior in TLA, 59 00:02:49,390 --> 00:02:52,509 as you should know, is an infinite sequence of states. 60 00:02:52,509 --> 00:02:56,275 Each state a mapping from variables to values. 61 00:02:56,275 --> 00:03:00,805 Our formula only mentions a finite small set of variables, 62 00:03:00,805 --> 00:03:03,580 but the class of satisfied behaviors contain 63 00:03:03,580 --> 00:03:07,105 those that assign any arbitrary value to any variable, 64 00:03:07,105 --> 00:03:09,860 not mentioned in the formula at each state. 65 00:03:09,860 --> 00:03:13,820 In other words, the formula describes all those behaviors of 66 00:03:13,820 --> 00:03:18,600 an entire world that contains our system of interest. 67 00:03:18,760 --> 00:03:23,230 If formula F describes a world containing one system, 68 00:03:23,230 --> 00:03:25,995 and formula G a world containing another, 69 00:03:25,995 --> 00:03:27,950 then a world containing both will 70 00:03:27,950 --> 00:03:29,760 be an intersection of those worlds, 71 00:03:29,760 --> 00:03:32,810 and it is described by the formula that is 72 00:03:32,810 --> 00:03:36,780 the conjunction of F and G. In this way, 73 00:03:36,780 --> 00:03:39,320 conjunction in TLA describes any form of 74 00:03:39,320 --> 00:03:42,725 composition of two or more systems or components. 75 00:03:42,725 --> 00:03:45,110 Or if they interact in any way, 76 00:03:45,110 --> 00:03:48,815 then they must share some of the variables they mentioned. 77 00:03:48,815 --> 00:03:51,950 That conjunction is such as simple expression of 78 00:03:51,950 --> 00:03:55,400 composition in TLA has some immediate consequences. 79 00:03:55,400 --> 00:03:58,130 For example, it has immediate results of 80 00:03:58,130 --> 00:04:01,445 propositional logic that if F implies A, 81 00:04:01,445 --> 00:04:04,595 meaning that the property A [inaudible] in Fs world, 82 00:04:04,595 --> 00:04:08,040 and G implies B, then the conjunction of F 83 00:04:08,040 --> 00:04:12,445 and G implies both A and B. 84 00:04:12,445 --> 00:04:14,525 This is always true, 85 00:04:14,525 --> 00:04:15,965 but we must be careful, 86 00:04:15,965 --> 00:04:17,945 as it could be true vacuously. 87 00:04:17,945 --> 00:04:20,960 The intersection of the two worlds could be empty if 88 00:04:20,960 --> 00:04:24,955 the conjunction of the two formulas is equivalent to false. 89 00:04:24,955 --> 00:04:27,650 This is the one downside of TLAs 90 00:04:27,650 --> 00:04:31,165 elegant formalization of composition that I can think of. 91 00:04:31,165 --> 00:04:34,400 Unfortunately, while it is possible to check if 92 00:04:34,400 --> 00:04:38,045 a specific formula's equal to false in TLC, 93 00:04:38,045 --> 00:04:40,160 TLC does not currently offer 94 00:04:40,160 --> 00:04:43,010 a way to do it generally and automatically, 95 00:04:43,010 --> 00:04:44,405 even though it could, 96 00:04:44,405 --> 00:04:45,960 by allowing us to check if 97 00:04:45,960 --> 00:04:48,829 the specification implies a false property. 98 00:04:48,829 --> 00:04:51,905 I think it should and hope it will. 99 00:04:51,905 --> 00:04:56,330 We will be looking at conjunctions of canonical forms. 100 00:04:56,330 --> 00:04:58,955 They don't specify one state machine, 101 00:04:58,955 --> 00:05:02,195 but a composition of two or possibly more. 102 00:05:02,195 --> 00:05:05,360 This can be used to write a composed specification, 103 00:05:05,360 --> 00:05:07,370 and we'll see one example of that. 104 00:05:07,370 --> 00:05:08,870 But because TLA doesn't 105 00:05:08,870 --> 00:05:11,330 distinguish between systems and properties, 106 00:05:11,330 --> 00:05:15,785 it can also be used to specify and check interesting properties. 107 00:05:15,785 --> 00:05:19,040 To be able to check such a formula in TLC, 108 00:05:19,040 --> 00:05:22,550 we'll need to transform it into the canonical form. 109 00:05:22,550 --> 00:05:24,440 In the next few slides, 110 00:05:24,440 --> 00:05:26,960 I will use colors to distinguish clauses 111 00:05:26,960 --> 00:05:30,155 rather than subscripts like init 1 and init 2. 112 00:05:30,155 --> 00:05:32,640 I hope that will be cleared. 113 00:05:33,830 --> 00:05:39,180 First, we rewrite our formula like so. 114 00:05:39,910 --> 00:05:43,250 Then we see that most of it can 115 00:05:43,250 --> 00:05:46,190 be easily copied into a canonical formula. 116 00:05:46,190 --> 00:05:50,045 The initial saint predicate and the fairness conditions. 117 00:05:50,045 --> 00:05:51,950 But the problem is the middle parts 118 00:05:51,950 --> 00:05:54,800 containing the temporal operator and the action. 119 00:05:54,800 --> 00:06:00,510 Because a canonical formula allows only one box action clause. 120 00:06:02,050 --> 00:06:06,560 To rewrite the two box action clauses into one, 121 00:06:06,560 --> 00:06:09,220 we'll use some logical identities. 122 00:06:09,220 --> 00:06:11,900 Number 1, we know from 123 00:06:11,900 --> 00:06:14,300 propositional logic that conjunction and 124 00:06:14,300 --> 00:06:17,260 disjunction distribute to [inaudible] one another. 125 00:06:17,260 --> 00:06:21,020 Number 2, we know that in temporal logic, 126 00:06:21,020 --> 00:06:27,020 box A and box B is equal to box A and B. 127 00:06:27,020 --> 00:06:29,795 Finally, we know in TLA, 128 00:06:29,795 --> 00:06:34,310 box square brackets action_vars is 129 00:06:34,310 --> 00:06:39,575 equal to box action or unchanged vars. 130 00:06:39,575 --> 00:06:44,015 The shaded area has formulas that aren't well-formed in TLA, 131 00:06:44,015 --> 00:06:47,700 but we can use them to make a correct deduction. 132 00:06:48,590 --> 00:06:51,650 Using those identities, we can 133 00:06:51,650 --> 00:06:55,070 rewrite the two box action clauses into one. 134 00:06:55,070 --> 00:07:02,785 We get this, and then this well-formed TLA expression. 135 00:07:02,785 --> 00:07:07,285 If one set of variables is contained in the other, 136 00:07:07,285 --> 00:07:10,899 we can eliminate either the second or third disjunct 137 00:07:10,899 --> 00:07:12,850 because it will equal false, 138 00:07:12,850 --> 00:07:15,325 and if the two sets of variables are the same, 139 00:07:15,325 --> 00:07:19,295 we can eliminate both and just remain with a first disjunct. 140 00:07:19,295 --> 00:07:22,660 With this, we now know how to conjoin 141 00:07:22,660 --> 00:07:26,920 two canonical formulas into one canonical formula in TLA. 142 00:07:26,920 --> 00:07:29,650 What can we do in TLA plus, 143 00:07:29,650 --> 00:07:34,310 and in particular, in a way that is checkable by TLC? 144 00:07:35,580 --> 00:07:38,680 We begin by writing the result 145 00:07:38,680 --> 00:07:41,250 from the previous slide as a definition. 146 00:07:41,250 --> 00:07:44,375 But this doesn't quite work with TLC. 147 00:07:44,375 --> 00:07:48,590 The reason is that when TLC evaluates an expression, 148 00:07:48,590 --> 00:07:52,805 it requires that the first time it encounters a prime variable, 149 00:07:52,805 --> 00:07:55,800 possibly after skipping arbitrary disjunct, 150 00:07:55,800 --> 00:07:59,255 it must appear in the form x equals something, 151 00:07:59,255 --> 00:08:01,640 or x is a member of something. 152 00:08:01,640 --> 00:08:05,449 This might not be the case here in the second and third disjunct, 153 00:08:05,449 --> 00:08:08,980 even if we write NextA and NextB carefully. 154 00:08:08,980 --> 00:08:14,525 Fortunately, unchanged x is interpreted as x prime equals x. 155 00:08:14,525 --> 00:08:20,040 All we need to do is change the order of our conjuncts. 156 00:08:20,150 --> 00:08:25,090 We put unchanged first and we're done. 157 00:08:27,150 --> 00:08:30,160 Instead of writing the first back, 158 00:08:30,160 --> 00:08:32,620 we write the equivalent bottom one that 159 00:08:32,620 --> 00:08:35,830 is canonical and it can be checked by TLC. 160 00:08:35,830 --> 00:08:39,580 There might be some certainties with fairness, but to be honest, 161 00:08:39,580 --> 00:08:42,190 fairness is not needed in the examples I'll show you, 162 00:08:42,190 --> 00:08:44,140 so I didn't look into that and 163 00:08:44,140 --> 00:08:46,645 I'll leave out fairness in the rest of the talk. 164 00:08:46,645 --> 00:08:51,050 Now what if we want to compose more than two formulas? 165 00:08:51,120 --> 00:08:56,050 We just repeat, this actually works. 166 00:08:56,050 --> 00:08:58,690 By the way this is why I don't include the books in 167 00:08:58,690 --> 00:09:01,585 square brackets in definition of composed. 168 00:09:01,585 --> 00:09:06,110 That's the idea. Now what can we do with it? 169 00:09:08,600 --> 00:09:13,080 The first use case I'd like to show is specifications in 170 00:09:13,080 --> 00:09:14,865 the style of behavioral programming 171 00:09:14,865 --> 00:09:17,645 invented by David Harel and his students. 172 00:09:17,645 --> 00:09:20,140 Behavioral programming is a paradigm that 173 00:09:20,140 --> 00:09:22,330 Harel believes could make going from 174 00:09:22,330 --> 00:09:25,180 specification to implementation easier 175 00:09:25,180 --> 00:09:28,375 in iterative and interactive process. 176 00:09:28,375 --> 00:09:31,960 The idea is that we write a program by gradually 177 00:09:31,960 --> 00:09:35,620 layering rules with different priorities on top of each other. 178 00:09:35,620 --> 00:09:37,360 To change the program, 179 00:09:37,360 --> 00:09:40,165 we add a new rule that refines is. 180 00:09:40,165 --> 00:09:44,065 The rules are actually called behaviors or behavior threads, 181 00:09:44,065 --> 00:09:46,630 each of which corresponds quite nicely 182 00:09:46,630 --> 00:09:49,554 to a state machines specification in TLA, 183 00:09:49,554 --> 00:09:51,640 and the layering of rules corresponds 184 00:09:51,640 --> 00:09:54,250 to conjoining canonical formulas. 185 00:09:54,250 --> 00:09:55,930 In this use case, 186 00:09:55,930 --> 00:09:57,370 we are actually going to write 187 00:09:57,370 --> 00:10:01,045 a specification as a conjunction of canonical formulas. 188 00:10:01,045 --> 00:10:03,789 The paper gives an example of specifying 189 00:10:03,789 --> 00:10:06,940 slash programming the game of Tic-Tac-Toe, 190 00:10:06,940 --> 00:10:08,830 and using what I showed you, 191 00:10:08,830 --> 00:10:11,560 I was able to specify the game until a plus in 192 00:10:11,560 --> 00:10:15,130 the gradual iterative style of behavioral programming. 193 00:10:15,130 --> 00:10:17,500 I will go over the example very quickly 194 00:10:17,500 --> 00:10:19,630 just to give you a taste of the idea. 195 00:10:19,630 --> 00:10:23,260 There is no need to carefully read the spec snippet on the slides, 196 00:10:23,260 --> 00:10:26,450 I'll point out the important bits. 197 00:10:26,910 --> 00:10:31,900 We begin by specifying a three-by-three board, 198 00:10:31,900 --> 00:10:34,240 where each set if there is 199 00:10:34,240 --> 00:10:38,260 a free square an X or an O piece is placed in it. 200 00:10:38,260 --> 00:10:40,750 We can already say to property that says that 201 00:10:40,750 --> 00:10:46,850 the fill square is never vacated and check it with TLC. 202 00:10:48,150 --> 00:10:53,230 We then know a rule that enforces alternating terms, 203 00:10:53,230 --> 00:10:57,415 first, X plays then O and so on. 204 00:10:57,415 --> 00:10:59,170 This rule is expressed as 205 00:10:59,170 --> 00:11:02,785 a separate state machine in the formula enforce turns, 206 00:11:02,785 --> 00:11:05,980 which is then conjoined to the previous factor form 207 00:11:05,980 --> 00:11:08,200 Tic-Tac-Toe 2 that we can 208 00:11:08,200 --> 00:11:11,540 check once we apply the technique we learned. 209 00:11:12,810 --> 00:11:18,055 We then add a rule, another state machine detect when, 210 00:11:18,055 --> 00:11:20,650 that detects a win or a drawer. 211 00:11:20,650 --> 00:11:22,660 We can again can join it to 212 00:11:22,660 --> 00:11:26,020 Tic-Tac-Toe 2 and check some properties. 213 00:11:26,020 --> 00:11:28,270 If we play like this, 214 00:11:28,270 --> 00:11:30,505 the players making arbitrary moves, 215 00:11:30,505 --> 00:11:33,740 this is a TLC output beget. 216 00:11:35,490 --> 00:11:38,575 But now we start adding tactics, 217 00:11:38,575 --> 00:11:41,800 each has its own rule and canonical formula that we can 218 00:11:41,800 --> 00:11:45,640 join to the previous one and that we can check its every step. 219 00:11:45,640 --> 00:11:48,880 First we say that if a player can complete 220 00:11:48,880 --> 00:11:52,970 line by marking an empty square, they do it. 221 00:11:55,200 --> 00:11:58,210 Then we add a rule that if we can block 222 00:11:58,210 --> 00:12:00,685 the opponent from winning in the next turn, 223 00:12:00,685 --> 00:12:03,160 we'll do it, but we give it 224 00:12:03,160 --> 00:12:07,190 a lower priority than completing our own line in winning. 225 00:12:10,320 --> 00:12:13,690 Then we add a lower priority rule, 226 00:12:13,690 --> 00:12:18,700 that if the center square is free we place our square there. 227 00:12:18,700 --> 00:12:21,130 Here for example, we can check that 228 00:12:21,130 --> 00:12:25,910 the first move will always place a piece in the center square. 229 00:12:27,060 --> 00:12:30,400 Finally, we add a rule with a lower priority, 230 00:12:30,400 --> 00:12:36,260 so that says that if a corner is free place a piece there. 231 00:12:36,630 --> 00:12:40,300 At these points, we can already check that the rules we 232 00:12:40,300 --> 00:12:44,450 have so far will always lead to a draw. 233 00:12:46,830 --> 00:12:49,345 To check each of these tabs, 234 00:12:49,345 --> 00:12:51,400 we can join the spanks as we learned, 235 00:12:51,400 --> 00:12:54,730 and this is the full spank containing all seven rules. 236 00:12:54,730 --> 00:12:57,685 Checking it with all the interesting properties 237 00:12:57,685 --> 00:13:00,595 takes only about seven seconds on my machine. 238 00:13:00,595 --> 00:13:03,129 Obviously, there are fewer states 239 00:13:03,129 --> 00:13:06,230 than when we play without tactics. 240 00:13:06,870 --> 00:13:09,220 Now I don't know if this sounds 241 00:13:09,220 --> 00:13:11,650 specification is helpful in TLA plus. 242 00:13:11,650 --> 00:13:14,155 My conclusion from this particular example 243 00:13:14,155 --> 00:13:16,030 is that perhaps not so much, 244 00:13:16,030 --> 00:13:18,775 but maybe this specification is too simple, 245 00:13:18,775 --> 00:13:23,035 you can find the full specification here and judge for yourself. 246 00:13:23,035 --> 00:13:26,125 But I think it's cool that we can use TLC to check 247 00:13:26,125 --> 00:13:27,970 at least some specifications that are 248 00:13:27,970 --> 00:13:30,700 not in the canonical state machine style. 249 00:13:30,700 --> 00:13:33,370 Here are some resources where you 250 00:13:33,370 --> 00:13:36,590 can learn more about behavioral programming. 251 00:13:39,000 --> 00:13:41,215 In the next example, 252 00:13:41,215 --> 00:13:44,590 we're not going to use conjunction to write a specification, 253 00:13:44,590 --> 00:13:47,125 but rather to check a special property 254 00:13:47,125 --> 00:13:49,255 called a possibility property. 255 00:13:49,255 --> 00:13:53,480 The idea is based on a paper by Leslie Lamport. 256 00:13:54,150 --> 00:13:57,115 A possibility property asks, 257 00:13:57,115 --> 00:13:59,470 ''Is it always possible to get from 258 00:13:59,470 --> 00:14:03,340 any reachable state of the system to some state P?'' 259 00:14:03,340 --> 00:14:06,250 In the paper, Lamport says that while 260 00:14:06,250 --> 00:14:08,050 possibility properties are not as 261 00:14:08,050 --> 00:14:10,975 important as safety or liveness properties, 262 00:14:10,975 --> 00:14:14,540 they can be of interest as a sanity check. 263 00:14:16,080 --> 00:14:20,020 TLA, being a linear temporal logic, 264 00:14:20,020 --> 00:14:23,230 does not allow to directly express possibility, 265 00:14:23,230 --> 00:14:27,205 but Lamport shows that if the possibility property holds, 266 00:14:27,205 --> 00:14:29,950 it is always possible to find some new action 267 00:14:29,950 --> 00:14:35,650 M with associated fairness G that restricts and directs 268 00:14:35,650 --> 00:14:38,155 the state machines next state action 269 00:14:38,155 --> 00:14:41,050 to take us from any ometer reachable state of 270 00:14:41,050 --> 00:14:44,230 the system to the state P. This is 271 00:14:44,230 --> 00:14:47,935 a process analogous to existential quantifier elimination, 272 00:14:47,935 --> 00:14:51,830 and then this is a proposition we need to prove. 273 00:14:53,460 --> 00:14:57,445 While the spec is given as a canonical formula, 274 00:14:57,445 --> 00:14:59,650 the proposition isn't canonical. 275 00:14:59,650 --> 00:15:03,340 We have a conjunction with another temporal subformula. 276 00:15:03,340 --> 00:15:06,085 But unlike the previous example, 277 00:15:06,085 --> 00:15:09,130 we have this diamond operator here, 278 00:15:09,130 --> 00:15:11,275 but we can't get rid of it. 279 00:15:11,275 --> 00:15:15,985 It means that at some points the M action starts occurring, 280 00:15:15,985 --> 00:15:18,205 restricting the next action, 281 00:15:18,205 --> 00:15:20,980 so we can recreate the same effect with 282 00:15:20,980 --> 00:15:25,100 additional variable and another fairness condition. 283 00:15:25,500 --> 00:15:31,645 We add a new Boolean variable T initialized to false, 284 00:15:31,645 --> 00:15:34,030 and we add a fairness condition 285 00:15:34,030 --> 00:15:37,240 that says that eventually it will become true, 286 00:15:37,240 --> 00:15:42,190 this will trigger the operation of M. Now, 287 00:15:42,190 --> 00:15:47,870 we have a conjunction of canonical formulas that we can check. 288 00:15:50,870 --> 00:15:54,300 We then notice that the set of variables 289 00:15:54,300 --> 00:15:57,690 vars is a subset of vars union t, 290 00:15:57,690 --> 00:16:00,810 and so one of the disjuncts in the composition drops 291 00:16:00,810 --> 00:16:02,940 off and after a few steps of 292 00:16:02,940 --> 00:16:05,400 rewriting that I'm skipping, for example, 293 00:16:05,400 --> 00:16:09,615 I wanted to take the unchanged t clause outside the parentheses, 294 00:16:09,615 --> 00:16:12,855 so I introduced the sub-action trigger 295 00:16:12,855 --> 00:16:15,120 that triggers the operation of 296 00:16:15,120 --> 00:16:18,030 M. We get this canonical formula 297 00:16:18,030 --> 00:16:21,240 and the proposition that we can then check in TLC. 298 00:16:21,240 --> 00:16:23,490 I haven't actually tried this because 299 00:16:23,490 --> 00:16:25,530 I don't have a good example to try it on. 300 00:16:25,530 --> 00:16:28,870 But if you come up with one, send it my way. 301 00:16:30,730 --> 00:16:33,149 In the final example, 302 00:16:33,149 --> 00:16:35,175 we're also going to use conjunction, 303 00:16:35,175 --> 00:16:37,380 not to specify but to check. 304 00:16:37,380 --> 00:16:39,240 Only this time, it's not going to be 305 00:16:39,240 --> 00:16:41,040 a property of the specification, 306 00:16:41,040 --> 00:16:43,064 but of a real system. 307 00:16:43,064 --> 00:16:46,080 One of the questions we often hear from TLA plus 308 00:16:46,080 --> 00:16:48,915 newcomers and not just newcomers is, 309 00:16:48,915 --> 00:16:53,160 how do I know that my system conforms to the specification? 310 00:16:53,160 --> 00:16:57,210 While humanity currently lacks the technology to soundly verify 311 00:16:57,210 --> 00:16:59,700 spec conformance on systems of 312 00:16:59,700 --> 00:17:03,285 size that TLA plus is routinely use to specify, 313 00:17:03,285 --> 00:17:06,225 perhaps there is some way to test conformance 314 00:17:06,225 --> 00:17:09,465 that is more mechanical than just by inspection. 315 00:17:09,465 --> 00:17:12,300 There might not be sound but at least could be 316 00:17:12,300 --> 00:17:16,260 useful in effectively finding bugs in the implementation. 317 00:17:16,260 --> 00:17:21,690 One such technique is called Model-Based Trace-Checking. 318 00:17:21,690 --> 00:17:26,429 The idea is to gather logs of execution traces from a real system, 319 00:17:26,429 --> 00:17:28,755 the implementation language doesn't matter, 320 00:17:28,755 --> 00:17:30,810 and using model checker to find 321 00:17:30,810 --> 00:17:34,665 inconsistencies between the traces in the specified model. 322 00:17:34,665 --> 00:17:37,379 Of course, because its traces are finite, 323 00:17:37,379 --> 00:17:41,230 we can only check for violations of safety properties. 324 00:17:41,480 --> 00:17:48,000 In TLA, a specification G conforms with F, or implements F, 325 00:17:48,000 --> 00:17:51,360 or refines F if the clause of behaviors 326 00:17:51,360 --> 00:17:54,974 G allows is contained in those F allows. 327 00:17:54,974 --> 00:17:57,900 Formally, this happens when G implies 328 00:17:57,900 --> 00:18:02,625 F. This by the way is my favorite feature of TLA, 329 00:18:02,625 --> 00:18:05,985 that the abstraction refinement relation 330 00:18:05,985 --> 00:18:08,805 is expressed as ordinary implication. 331 00:18:08,805 --> 00:18:13,200 We would be able to soundly check if a real system implementation 332 00:18:13,200 --> 00:18:15,060 conforms with the spec if 333 00:18:15,060 --> 00:18:18,150 all of it's behaviors are allowed by the spec. 334 00:18:18,150 --> 00:18:21,945 Instead, we check that only some of it's behaviors, 335 00:18:21,945 --> 00:18:23,940 those that come from execution traces 336 00:18:23,940 --> 00:18:27,210 extracted from log files, satisfy the spec. 337 00:18:27,210 --> 00:18:30,105 Just remember that a single trace 338 00:18:30,105 --> 00:18:32,549 doesn't represent a single TLA behavior, 339 00:18:32,549 --> 00:18:34,215 but a whole class. 340 00:18:34,215 --> 00:18:36,404 Aside from matter of suturing, 341 00:18:36,404 --> 00:18:40,155 the trace allows any unmentioned variable to take any value. 342 00:18:40,155 --> 00:18:42,540 We're still talking about classes of 343 00:18:42,540 --> 00:18:47,770 behaviors which we could then represent with a TLA plus formula. 344 00:18:48,950 --> 00:18:53,625 Let's begin with a specification of a simple system. 345 00:18:53,625 --> 00:18:57,210 We have a clock that goes tick tock. 346 00:18:57,210 --> 00:18:59,430 Every time it ticks, 347 00:18:59,430 --> 00:19:04,200 x and y are assigned an arbitrary value between zero and nine, 348 00:19:04,200 --> 00:19:06,119 and every time it tocks, 349 00:19:06,119 --> 00:19:09,150 z is assigned the sum of x and y. 350 00:19:09,150 --> 00:19:14,739 TLC tells us that this system has 2,000 states. 351 00:19:16,370 --> 00:19:18,855 For the purpose of demonstration, 352 00:19:18,855 --> 00:19:20,850 I will embed the trace directly in the TLA 353 00:19:20,850 --> 00:19:23,535 plus file as a sequence of tuples. 354 00:19:23,535 --> 00:19:25,455 Of course, in real usage, 355 00:19:25,455 --> 00:19:28,530 we'll probably want to write a TLC operator override in 356 00:19:28,530 --> 00:19:32,160 Java that will read the trace directly from a log file, 357 00:19:32,160 --> 00:19:35,490 and I believe some people have already written such operators and 358 00:19:35,490 --> 00:19:40,210 contributed them to the TLA plus community modules. 359 00:19:41,480 --> 00:19:44,430 We could write the formula that expresses 360 00:19:44,430 --> 00:19:47,955 the trace as behaviors in TLA plus like so. 361 00:19:47,955 --> 00:19:50,955 We instantiate the system spec, 362 00:19:50,955 --> 00:19:53,895 we define a read operation, 363 00:19:53,895 --> 00:19:56,685 we start by reading the first entry, 364 00:19:56,685 --> 00:19:58,215 and then at each step, 365 00:19:58,215 --> 00:20:01,605 we read another until there's none left. 366 00:20:01,605 --> 00:20:05,055 There are several things that TLC doesn't like here. 367 00:20:05,055 --> 00:20:09,000 It doesn't like the tuple equality in the initial [inaudible]. 368 00:20:09,000 --> 00:20:11,070 And it doesn't like a primed operator as 369 00:20:11,070 --> 00:20:13,635 the first occurrence of a prime variable. 370 00:20:13,635 --> 00:20:19,150 It also doesn't let us directly use Model!vars. 371 00:20:20,810 --> 00:20:23,820 To make this work with TLC, 372 00:20:23,820 --> 00:20:25,380 we write the formula in 373 00:20:25,380 --> 00:20:28,230 a more cumbersome and less general way with 374 00:20:28,230 --> 00:20:34,060 this Read and ReadNext definitions but it works. 375 00:20:34,490 --> 00:20:37,425 Then to check conformance, 376 00:20:37,425 --> 00:20:40,980 we simply check that this holds. 377 00:20:40,980 --> 00:20:43,845 I want to point out two things here. 378 00:20:43,845 --> 00:20:47,505 First, because we're only dealing with finite traces, 379 00:20:47,505 --> 00:20:51,225 we can only check conformance with the safety part of the system. 380 00:20:51,225 --> 00:20:55,065 We also turn off deadlock detection in TLC. 381 00:20:55,065 --> 00:20:58,755 Second, because we're just checking the trace, 382 00:20:58,755 --> 00:21:02,310 then it doesn't matter how complex our system spec is. 383 00:21:02,310 --> 00:21:07,110 The number of states is determined by the trace, not the system. 384 00:21:07,110 --> 00:21:09,750 The trace has 20 records and TLC 385 00:21:09,750 --> 00:21:13,809 finds 20 states arranged linearly. 386 00:21:15,730 --> 00:21:18,650 We can do even better and exploit 387 00:21:18,650 --> 00:21:21,380 TLC to check many traces at once. 388 00:21:21,380 --> 00:21:23,750 Suppose we have multiple log files. 389 00:21:23,750 --> 00:21:25,985 Again, for the purpose of demonstration, 390 00:21:25,985 --> 00:21:30,085 here I've embedded them in the TLA plus specification. 391 00:21:30,085 --> 00:21:33,870 This is how we turn the traces into a formula. 392 00:21:33,870 --> 00:21:36,630 The only thing that's changed from before is 393 00:21:36,630 --> 00:21:39,825 I've added another index variable, log, 394 00:21:39,825 --> 00:21:43,650 that is non-deterministically chosen at 395 00:21:43,650 --> 00:21:49,180 the initial state and then remains unchanged during the behavior. 396 00:21:49,220 --> 00:21:52,635 Again, we check and we get 397 00:21:52,635 --> 00:21:57,390 a small state space that looks unsurprisingly like this. 398 00:21:57,390 --> 00:21:59,220 So far so good, 399 00:21:59,220 --> 00:22:00,975 but we haven't done anything interesting 400 00:22:00,975 --> 00:22:03,790 with conjunction just yet. 401 00:22:05,030 --> 00:22:07,740 Here the plot thickens. 402 00:22:07,740 --> 00:22:09,810 Supposing a log file only 403 00:22:09,810 --> 00:22:12,735 records some of the variables in our system. 404 00:22:12,735 --> 00:22:16,275 For example, suppose it only logs a value of z. 405 00:22:16,275 --> 00:22:19,590 Does such a trace conform to our spec nodes? 406 00:22:19,590 --> 00:22:26,460 Does our model allow for such an observable behaviors of z? 407 00:22:26,460 --> 00:22:30,030 We really want to check this with a variables x, y, 408 00:22:30,030 --> 00:22:34,455 and tickTock, treated as hidden on observed variables. 409 00:22:34,455 --> 00:22:38,340 It means that for every behavior and trace behavior, 410 00:22:38,340 --> 00:22:43,380 there exists a corresponding behavior that satisfies Model!Safety 411 00:22:43,380 --> 00:22:49,020 with matching values for z and some values for x, y, and tickTock. 412 00:22:49,020 --> 00:22:52,950 But TLC can't check properties with temporal quantifiers. 413 00:22:52,950 --> 00:22:54,990 So we need to get rid of it somehow. 414 00:22:54,990 --> 00:22:58,230 Ordinarily, we'd eliminate the temporal 415 00:22:58,230 --> 00:23:02,310 existential by constructing the sought-after behavior ourselves, 416 00:23:02,310 --> 00:23:04,170 adding auxiliary variables in 417 00:23:04,170 --> 00:23:05,880 a refinement mapping to fill in 418 00:23:05,880 --> 00:23:08,830 the values for the hidden variables. 419 00:23:09,110 --> 00:23:12,765 We read the trace as before. 420 00:23:12,765 --> 00:23:17,130 But to turn it into a formula we can check against a system model, 421 00:23:17,130 --> 00:23:20,775 we add an auxiliary variable tt that 422 00:23:20,775 --> 00:23:24,660 adds a suturing step to mimic the ticks and the tocks. 423 00:23:24,660 --> 00:23:31,875 Then we conjure appropriate values for x and y. This works. 424 00:23:31,875 --> 00:23:34,545 But as those of you who tried it know, 425 00:23:34,545 --> 00:23:36,210 adding a refinement mapping and 426 00:23:36,210 --> 00:23:39,150 auxiliary variables is not always easy. 427 00:23:39,150 --> 00:23:41,700 Ordinarily, we don't have a choice. 428 00:23:41,700 --> 00:23:43,080 But in this case, 429 00:23:43,080 --> 00:23:45,479 we can use the unique properties of a trace 430 00:23:45,479 --> 00:23:49,810 combined with the power of conjunction to do the work for us. 431 00:23:50,570 --> 00:23:53,640 This is what we want to check. 432 00:23:53,640 --> 00:23:58,170 To use TLC, we must still eliminate that temporal quantifier, 433 00:23:58,170 --> 00:24:00,675 but we wanted it automatically. 434 00:24:00,675 --> 00:24:03,750 We notice something special about trace behavior. 435 00:24:03,750 --> 00:24:05,535 Even though, as I mentioned, 436 00:24:05,535 --> 00:24:08,220 it corresponds to some infinite class of behaviors, 437 00:24:08,220 --> 00:24:09,750 we can think of it as 438 00:24:09,750 --> 00:24:13,275 a single behavior as far as our variables are concerned. 439 00:24:13,275 --> 00:24:15,330 This is a little hand-wavy and 440 00:24:15,330 --> 00:24:18,490 the details include equivalence classes. 441 00:24:18,500 --> 00:24:25,095 The proposition is true if Model!Safety contains trace behavior. 442 00:24:25,095 --> 00:24:27,330 But because there is effectively 443 00:24:27,330 --> 00:24:29,655 just one element and trace behavior, 444 00:24:29,655 --> 00:24:34,230 this happens if and only if their conjunction is not empty. 445 00:24:34,230 --> 00:24:38,280 This is analogous to a set with one element that is 446 00:24:38,280 --> 00:24:40,380 contained in another set if and only 447 00:24:40,380 --> 00:24:43,540 if their intersection is not empty. 448 00:24:44,780 --> 00:24:48,690 That's equivalent to saying that it is 449 00:24:48,690 --> 00:24:52,395 not a theorem that this conjunction is equal to false, 450 00:24:52,395 --> 00:24:54,600 which is equivalent to saying that it is not 451 00:24:54,600 --> 00:24:58,530 a theorem that the conjunction implies false. 452 00:24:58,530 --> 00:25:00,225 Thanks to what we know, 453 00:25:00,225 --> 00:25:03,460 this is something we can check. 454 00:25:04,610 --> 00:25:08,310 We use the conjunction technique to define 455 00:25:08,310 --> 00:25:12,190 the conjoin formula in a way that TLC can check, 456 00:25:12,190 --> 00:25:15,470 and then we need to check that this is not false. 457 00:25:15,470 --> 00:25:16,880 As I mentioned before, 458 00:25:16,880 --> 00:25:18,650 TLC does not currently allow us to 459 00:25:18,650 --> 00:25:20,570 check if a formula implies false. 460 00:25:20,570 --> 00:25:22,040 I hope it will someday. 461 00:25:22,040 --> 00:25:25,765 But that's okay because we can always find something equivalent. 462 00:25:25,765 --> 00:25:29,189 We pick a property that must be true for every behavior, 463 00:25:29,189 --> 00:25:31,200 so that asserting it isn't true is 464 00:25:31,200 --> 00:25:34,215 equivalent to saying that our specification is false. 465 00:25:34,215 --> 00:25:37,455 Because we want to show that this is not a theorem, 466 00:25:37,455 --> 00:25:40,530 we challenge TLC to find a counterexample. 467 00:25:40,530 --> 00:25:43,740 If it finds one, we know that the conjunction is not 468 00:25:43,740 --> 00:25:48,255 empty and that our trace does conform to our system model, 469 00:25:48,255 --> 00:25:51,825 and this is indeed what we find. 470 00:25:51,825 --> 00:25:54,015 But notice what we get. 471 00:25:54,015 --> 00:25:58,935 TLC explores many more states than there are in the trace, 472 00:25:58,935 --> 00:26:00,930 but far fewer states than there are in 473 00:26:00,930 --> 00:26:04,445 the system that I pasted here below for reference. 474 00:26:04,445 --> 00:26:06,710 TLC finds a violation of 475 00:26:06,710 --> 00:26:09,110 the incorrect assertion that our conjunction is 476 00:26:09,110 --> 00:26:13,810 empty and that violation it finds matches our trace. 477 00:26:13,810 --> 00:26:16,905 If you look at the error trace TLC produces, 478 00:26:16,905 --> 00:26:18,810 it actually fills in conforming 479 00:26:18,810 --> 00:26:21,330 values of the hidden variables for us. 480 00:26:21,330 --> 00:26:25,995 It automatically a suturing steps for the ticks and the tocks, 481 00:26:25,995 --> 00:26:30,400 and it automatically finds values for x and y. 482 00:26:32,360 --> 00:26:36,195 You can find the full specification here. 483 00:26:36,195 --> 00:26:40,155 How effective is this technique in finding bugs in the real world? 484 00:26:40,155 --> 00:26:43,230 On the one hand, checking such a small portion of 485 00:26:43,230 --> 00:26:46,620 all system behaviors seems like a stab in the dark. 486 00:26:46,620 --> 00:26:49,140 On the other hand, perhaps 487 00:26:49,140 --> 00:26:52,695 many translation bugs are shallow and surface quickly. 488 00:26:52,695 --> 00:26:55,650 In any event, this technique might help localize 489 00:26:55,650 --> 00:26:59,160 bugs when analyzing traces known to be faulty. 490 00:26:59,160 --> 00:27:02,505 I'll leave it to others to find out and report. 491 00:27:02,505 --> 00:27:05,970 You can find modules with TLC operators that 492 00:27:05,970 --> 00:27:09,180 can read log files in the TLA plus community modules, 493 00:27:09,180 --> 00:27:10,560 and an example of using 494 00:27:10,560 --> 00:27:12,660 this technique in the wonderful walk-through 495 00:27:12,660 --> 00:27:16,990 tutorial of the TLA plus tools by Markus Kuppe. 496 00:27:17,360 --> 00:27:21,220 This is all. I hope you enjoyed.