spin.ms 66 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472147314741475147614771478147914801481148214831484148514861487148814891490149114921493149414951496149714981499150015011502150315041505150615071508150915101511151215131514151515161517151815191520152115221523152415251526152715281529153015311532153315341535153615371538153915401541154215431544154515461547154815491550155115521553155415551556155715581559156015611562156315641565156615671568156915701571157215731574157515761577157815791580158115821583158415851586158715881589159015911592159315941595159615971598159916001601160216031604160516061607160816091610161116121613161416151616161716181619162016211622162316241625162616271628162916301631163216331634163516361637163816391640164116421643164416451646164716481649165016511652165316541655165616571658165916601661166216631664166516661667166816691670167116721673167416751676167716781679168016811682168316841685168616871688168916901691169216931694169516961697169816991700170117021703170417051706170717081709171017111712171317141715171617171718171917201721172217231724172517261727172817291730173117321733173417351736173717381739174017411742174317441745174617471748174917501751175217531754175517561757175817591760176117621763176417651766176717681769177017711772177317741775177617771778177917801781178217831784178517861787178817891790179117921793179417951796179717981799180018011802180318041805180618071808180918101811181218131814181518161817181818191820182118221823182418251826182718281829183018311832183318341835183618371838183918401841184218431844184518461847184818491850185118521853185418551856185718581859186018611862186318641865186618671868186918701871187218731874187518761877187818791880188118821883188418851886188718881889189018911892189318941895189618971898189919001901190219031904190519061907190819091910191119121913191419151916191719181919192019211922192319241925192619271928192919301931193219331934193519361937193819391940194119421943194419451946194719481949195019511952195319541955195619571958195919601961196219631964196519661967196819691970197119721973197419751976197719781979198019811982198319841985198619871988198919901991199219931994199519961997199819992000200120022003200420052006200720082009201020112012201320142015201620172018201920202021202220232024202520262027202820292030203120322033203420352036203720382039204020412042204320442045204620472048204920502051205220532054205520562057205820592060206120622063206420652066206720682069207020712072207320742075207620772078207920802081208220832084208520862087208820892090209120922093209420952096209720982099210021012102210321042105210621072108210921102111211221132114211521162117211821192120212121222123212421252126212721282129213021312132213321342135213621372138213921402141214221432144214521462147214821492150215121522153215421552156215721582159216021612162216321642165216621672168216921702171217221732174217521762177217821792180218121822183218421852186218721882189219021912192219321942195219621972198219922002201220222032204220522062207220822092210221122122213221422152216221722182219222022212222222322242225222622272228222922302231223222332234223522362237223822392240224122422243224422452246224722482249225022512252225322542255225622572258225922602261226222632264226522662267226822692270227122722273227422752276227722782279228022812282228322842285228622872288228922902291229222932294229522962297229822992300230123022303230423052306230723082309231023112312231323142315231623172318231923202321232223232324232523262327232823292330233123322333233423352336233723382339234023412342234323442345234623472348234923502351235223532354235523562357235823592360236123622363236423652366236723682369237023712372237323742375237623772378237923802381238223832384238523862387238823892390239123922393239423952396239723982399240024012402240324042405240624072408240924102411241224132414241524162417241824192420242124222423242424252426242724282429243024312432243324342435243624372438243924402441244224432444244524462447244824492450245124522453245424552456245724582459246024612462246324642465246624672468246924702471247224732474247524762477247824792480248124822483248424852486248724882489249024912492249324942495249624972498249925002501250225032504250525062507250825092510251125122513251425152516251725182519
  1. .HTML "Using SPIN
  2. .\" runoff as:
  3. .\" eqn file | tbl | troff -ms
  4. .\"
  5. .ds P \\s-1PROMELA\\s0
  6. .ds V \\s-1SPIN\\s0
  7. .ds C pcc
  8. .\" .tr -\(hy
  9. .EQ
  10. delim $#
  11. .EN
  12. .TL
  13. Using \*V
  14. .AU
  15. Gerard J. Holzmann
  16. gerard@plan9.bell-labs.com
  17. .AB
  18. \*V can be used for proving or disproving logical properties
  19. of concurrent systems.
  20. To render the proofs, a concurrent system is first
  21. modeled in a formal specification language called \*P.
  22. The language allows one to specify the behaviors
  23. of asynchronously executing
  24. processes that may interact through synchronous
  25. or asynchronous message passing, or through direct
  26. access to shared variables.
  27. .LP
  28. System models specified in this way can be verified
  29. for both safety and liveness properties. The specification
  30. of general properties in linear time temporal logic is
  31. also supported.
  32. .LP
  33. The first part of this manual
  34. discusses the basic features of the specification language \*P.
  35. The second part describes the verifier \*V.
  36. .AE
  37. .NH 1
  38. The Language \*P
  39. .LP
  40. \*P is short for Protocol Meta Language [Ho91].
  41. \*P is a \f2modeling\f1 language, not a programming language.
  42. A formal model differs in two essential ways from an implementation.
  43. First, a model is meant to be an abstraction of a design
  44. that contains only those aspects of the design that are
  45. directly relevant to the properties one is interested in proving.
  46. Second, a formal model must contain things that are typically not part
  47. of an implementation, such as worst-case assumptions about
  48. the behavior of the environment that may interact with the
  49. system being studied, and a formal statement of relevant correctness
  50. properties. It is possible to mechanically extract abstract models
  51. from implementation level code, as discussed, for instance in [HS99].
  52. .LP
  53. Verification with \*V is often performed in a series of steps,
  54. with the construction of increasingly detailed models.
  55. Each model can be verified under different types of
  56. assumptions about the environment and for different
  57. types of correctness properties.
  58. If a property is not valid for the given assumptions about
  59. system behavior, the verifier can produce a counter-example
  60. that demonstrates how the property may be violated.
  61. If a property is valid, it may be possible to simplify the
  62. model based on that fact, and prove still other properties.
  63. .LP
  64. Section 1.1 covers the basic building blocks of the language.
  65. Section 1.2 introduces the control flow structures.
  66. Section 1.3 explains how correctness properties are specified.
  67. Section 1.4 concludes the first part with a discussion of
  68. special predefined variables and functions that can be used to
  69. express some correctness properties.
  70. .LP
  71. Up to date manual pages for \*V can always be found online at:
  72. .CW
  73. http://cm.bell-labs.com/cm/cs/what/spin/Man/
  74. .R
  75. .NH 2
  76. Basics
  77. .LP
  78. A \*P model can contain three different types of objects:
  79. .IP
  80. .RS
  81. \(bu Processes (section 1.1.1),
  82. .br
  83. \(bu Variables (section 1.1.2),
  84. .br
  85. \(bu Message channels (section 1.1.3).
  86. .RE
  87. .LP
  88. All processes are global objects.
  89. For obvious reasons, a \*P model must contain at least one
  90. process to be meaningful.
  91. Since \*V is specifically meant to prove properties of
  92. concurrent systems, a model typically contains more than
  93. one process.
  94. .LP
  95. Message channels and variables, the two basic types of data objects,
  96. can be declared with either a global scope or a local scope.
  97. A data object with global scope can be referred to by all processes.
  98. A data object with a local scope can be referred to by just a
  99. single process: the process that declares and instantiates the object.
  100. As usual, all objects must be declared in the specification
  101. before they are referenced.
  102. .NH 3
  103. Processes
  104. .LP
  105. Here is a simple process that does nothing except print
  106. a line of text:
  107. .P1
  108. init {
  109. printf("it works\en")
  110. }
  111. .P2
  112. There are a few things to note.
  113. .CW Init
  114. is a predefined keyword from the language.
  115. It can be used to declare and instantiate
  116. a single initial process in the model.
  117. (It is comparable to the
  118. .CW main
  119. procedure of a C program.)
  120. The
  121. .CW init
  122. process does not take arguments, but it can
  123. start up (instantiate) other processes that do.
  124. .CW Printf
  125. is one of a few built-in procedures in the language.
  126. It behaves the same as the C version.
  127. Note, finally, that no semicolon follows the single
  128. .CW printf
  129. statement in the above example.
  130. In \*P, semicolons are used as statement separators,
  131. not statement terminators. (The \*V parser, however, is
  132. lenient on this issue.)
  133. .LP
  134. Any process can start new processes by using another
  135. built-in procedure called
  136. .CW run .
  137. For example,
  138. .P1
  139. proctype you_run(byte x)
  140. {
  141. printf("my x is: %d\en", x)
  142. }
  143. .P2
  144. .P1
  145. init {
  146. run you_run(1);
  147. run you_run(2)
  148. }
  149. .P2
  150. The word
  151. .CW proctype
  152. is again a keyword that introduces the declaration
  153. of a new type of process.
  154. In this case, we have named that type
  155. .CW you_run
  156. and declared that all instantiations of processes
  157. of this type will take one argument: a data object
  158. of type
  159. .CW byte ,
  160. that can be referred to within this process by the name
  161. .CW x .
  162. Instances of a
  163. .CW proctype
  164. can be created with the predefined procedure
  165. .CW run ,
  166. as shown in the example.
  167. When the
  168. .CW run
  169. statement completes, a copy of the process
  170. has been started, and all its arguments have been
  171. initialized with the arguments provided.
  172. The process may, but need not, have performed
  173. any statement executions at this point.
  174. It is now part of the concurrent system,
  175. and its execution can be interleaved arbitrarily with
  176. those of the other, already executing processes.
  177. (More about the semantics of execution follows shortly.)
  178. .LP
  179. In many cases, we are only interested in creating a
  180. single instance of each process type that is declared,
  181. and the processes require no arguments.
  182. We can define this by prefixing the keyword
  183. .CW proctype
  184. from the process declaration with another keyword:
  185. .CW active .
  186. Instances of all active proctypes are created when the
  187. system itself is initialized.
  188. We could, for instance, have avoided the use of
  189. .CW init
  190. by declaring the corresponding process in the last example
  191. as follows:
  192. .P1
  193. active proctype main() {
  194. run you_run(1);
  195. run you_run(2)
  196. }
  197. .P2
  198. Note that there are no parameters to instantiate in this
  199. case. Had they been declared, they would default to a
  200. zero value, just like all other data objects
  201. that are not explicitly instantiated.
  202. .LP
  203. Multiple copies of a process type can also be created in
  204. this way. For example:
  205. .P1
  206. active [4] proctype try_me() {
  207. printf("hi, i am process %d\en", _pid)
  208. }
  209. .P2
  210. creates four processes.
  211. A predefined variable
  212. .CW _pid
  213. is assigned to each running process, and holds
  214. its unique process instantiation number.
  215. In some cases, this number is needed when a reference
  216. has to be made to a specific process.
  217. .LP
  218. Summarizing: process behavior is declared in
  219. .CW proctype
  220. definitions, and it is instantiated with either
  221. .CW run
  222. statements or with the prefix
  223. .CW active .
  224. Within a proctype declaration, statements are separated
  225. (not terminated) by semicolons.
  226. As we shall see in examples that follow, instead of the
  227. semicolon, one can also use the alternative separator
  228. .CW "->"
  229. (arrow), wherever that may help to clarify the structure
  230. of a \*P model.
  231. .SH
  232. Semantics of Execution
  233. .LP
  234. In \*P there is no difference between a condition or
  235. expression and a statement.
  236. Fundamental to the semantics of the language is the
  237. notion of the \f2executability\f1 of statements.
  238. Statements are either executable or blocked.
  239. Executability is the basic means of enforcing
  240. synchronization between the processes in a distributed system.
  241. A process can wait for an event to happen by waiting
  242. for a statement to become executable.
  243. For instance, instead of writing a busy wait loop:
  244. .P1
  245. while (a != b) /* not valid Promela syntax */
  246. skip; /* wait for a==b */
  247. \&...
  248. .P2
  249. we achieve the same effect in \*P with the statement
  250. .P1
  251. (a == b);
  252. \&...
  253. .P2
  254. Often we indicate that the continuation of an execution
  255. is conditional on the truth of some expression by using
  256. the alternate statement separator:
  257. .P1
  258. (a == b) -> \&...
  259. .P2
  260. Assignments and
  261. .CW printf
  262. statements are always executable in \*P.
  263. A condition, however, can only be executed (passed) when it holds.
  264. If the condition does not hold, execution blocks until it does.
  265. There are similar rules for determining the executability
  266. of all other primitive and compound statements in the
  267. language.
  268. The semantics of each statement is defined in terms of
  269. rules for executability and effect.
  270. The rules for executability set a precondition on the state
  271. of the system in which a statement can be executed.
  272. The effect defines how a statement will alter a
  273. system state when executed.
  274. .LP
  275. \*P assumes that all individual statements are executed
  276. atomically: that is, they model the smallest meaningful entities
  277. of execution in the system being studied.
  278. This means that \*P defines the standard asynchronous interleaving
  279. model of execution, where a supposed scheduler is free at
  280. each point in the execution to select any one of the processes
  281. to proceed by executing a single primitive statement.
  282. Synchronization constraints can be used to influence the
  283. interleaving patterns. It is the purpose of a concurrent system's
  284. design to constrain those patterns in such a way that no
  285. correctness requirements can be violated, and all service
  286. requirements are met. It is the purpose of the verifier
  287. either to find counter-examples to a designer's claim that this
  288. goal has been met, or to demonstrate that the claim is indeed valid.
  289. .NH 3
  290. Variables
  291. .LP
  292. The table summarizes the five basic data types used in \*P.
  293. .CW Bit
  294. and
  295. .CW bool
  296. are synonyms for a single bit of information.
  297. The first three types can store only unsigned quantities.
  298. The last two can hold either positive or negative values.
  299. The precise value ranges of variables of types
  300. .CW short
  301. and
  302. .CW int
  303. is implementation dependent, and corresponds
  304. to those of the same types in C programs
  305. that are compiled for the same hardware.
  306. The values given in the table are most common.
  307. .KS
  308. .TS
  309. center;
  310. l l
  311. lw(10) lw(12).
  312. =
  313. \f3Type Range\f1
  314. _
  315. bit 0..1
  316. bool 0..1
  317. byte 0..255
  318. short $-2 sup 15# .. $2 sup 15 -1#
  319. int $-2 sup 31# .. $2 sup 31 -1#
  320. _
  321. .TE
  322. .KE
  323. .LP
  324. The following example program declares a array of
  325. two elements of type
  326. .CW bool
  327. and a scalar variable
  328. .CW turn
  329. of the same type.
  330. Note that the example relies on the fact that
  331. .CW _pid
  332. is either 0 or 1 here.
  333. .MT _sec5critical
  334. .P1
  335. /*
  336. * Peterson's algorithm for enforcing
  337. * mutual exclusion between two processes
  338. * competing for access to a critical section
  339. */
  340. bool turn, want[2];
  341. active [2] proctype user()
  342. {
  343. again:
  344. want[_pid] = 1; turn = _pid;
  345. /* wait until this condition holds: */
  346. (want[1 - _pid] == 0 || turn == 1 - _pid);
  347. /* enter */
  348. critical: skip;
  349. /* leave */
  350. want[_pid] = 0;
  351. goto again
  352. }
  353. .P2
  354. In the above case, all variables are initialized to zero.
  355. The general syntax for declaring and instantiating a
  356. variable, respectively for scalar and array variables, is:
  357. .P1
  358. type name = expression;
  359. type name[constant] = expression
  360. .P2
  361. In the latter case, all elements of the array are initialized
  362. to the value of the expression.
  363. A missing initializer fields defaults to the value zero.
  364. As usual, multiple variables of the same type can be grouped
  365. behind a single type name, as in:
  366. .P1
  367. byte a, b[3], c = 4
  368. .P2
  369. In this example, the variable
  370. .CW c
  371. is initialized to the value 4; variable
  372. .CW a
  373. and the elements of array
  374. .CW b
  375. are all initialized to zero.
  376. .LP
  377. Variables can also be declared as structures.
  378. For example:
  379. .P1
  380. typedef Field {
  381. short f = 3;
  382. byte g
  383. };
  384. typedef Msg {
  385. byte a[3];
  386. int fld1;
  387. Field fld2;
  388. chan p[3];
  389. bit b
  390. };
  391. Msg foo;
  392. .P2
  393. introduces two user-defined data types, the first named
  394. .CW Field
  395. and the second named
  396. .CW Msg .
  397. A single variable named
  398. .CW foo
  399. of type
  400. .CW Msg
  401. is declared.
  402. All fields of
  403. .CW foo
  404. that are not explicitly initialized (in the example, all fields except
  405. .CW foo.fld2.f )
  406. are initialized to zero.
  407. References to the elements of a structure are written as:
  408. .P1
  409. foo.a[2] = foo.fld2.f + 12
  410. .P2
  411. A variable of a user-defined type can be passed as a single
  412. argument to a new process in
  413. .CW run
  414. statements.
  415. For instance,
  416. .P1
  417. proctype me(Msg z) {
  418. z.a[2] = 12
  419. }
  420. init {
  421. Msg foo;
  422. run me(foo)
  423. }
  424. .P2
  425. .LP
  426. Note that even though \*P supports only one-dimensional arrays,
  427. a two-dimensional array can be created indirectly with user-defined
  428. structures, for instance as follows:
  429. .P1
  430. typedef Array {
  431. byte el[4]
  432. };
  433. Array a[4];
  434. .P2
  435. This creates a data structure of 16 elements that can be
  436. referenced, for instance, as
  437. .CW a[i].el[j] .
  438. .LP
  439. As in C, the indices of an array of
  440. .CW N
  441. elements range from 0 to
  442. .CW N-1 .
  443. .SH
  444. Expressions
  445. .LP
  446. Expressions must be side-effect free in \*P.
  447. Specifically, this means that an expression cannot
  448. contain assignments, or send and receive operations (see section 1.1.3).
  449. .P1
  450. c = c + 1; c = c - 1
  451. .P2
  452. and
  453. .P1
  454. c++; c--
  455. .P2
  456. are assignments in \*P, with the same effects.
  457. But, unlike in C,
  458. .P1
  459. b = c++
  460. .P2
  461. is not a valid assignment, because the right-hand side
  462. operand is not a valid expression in \*P (it is not side-effect free).
  463. .LP
  464. It is also possible to write a side-effect free conditional
  465. expression, with the following syntax:
  466. .P1
  467. (expr1 -> expr2 : expr3)
  468. .P2
  469. The parentheses around the conditional expression are required to
  470. avoid misinterpretation of the arrow.
  471. The example expression has the value of \f(CWexpr2\f1 when \f(CWexpr1\f1
  472. evaluates to a non-zero value, and the value of \f(CWexpr3\f1 otherwise.
  473. .LP
  474. In assignments like
  475. .P1
  476. variable = expression
  477. .P2
  478. the values of all operands used inside the expression are first cast to
  479. signed integers before the operands are applied.
  480. After the evaluation of the expression completes, the value produced
  481. is cast to the type of the target variable before the assignment takes place.
  482. .NH 3
  483. Message Channels
  484. .LP
  485. Message channels are used to model the transfer of data
  486. between processes.
  487. They are declared either locally or globally,
  488. for instance as follows:
  489. .P1
  490. chan qname = [16] of { short, byte }
  491. .P2
  492. The keyword
  493. .CW chan
  494. introduces a channel declaration.
  495. In this case, the channel is named
  496. .CW qname ,
  497. and it is declared to be capable of storing up
  498. to 16 messages.
  499. Each message stored in the channel is declared here to
  500. consist of two fields: one of type
  501. .CW short
  502. and one of type
  503. .CW byte .
  504. The fields of a message can be any one of the basic types
  505. .CW bit ,
  506. .CW bool ,
  507. .CW byte ,
  508. .CW short ,
  509. .CW int ,
  510. and
  511. .CW chan ,
  512. or any user-defined type.
  513. Message fields cannot be declared as arrays.
  514. .LP
  515. A message field of type
  516. .CW chan
  517. can be used to pass a channel identifier
  518. through a channel from one process to another.
  519. .LP
  520. The statement
  521. .P1
  522. qname!expr1,expr2
  523. .P2
  524. sends the values of expressions
  525. .CW expr1
  526. and
  527. .CW expr2
  528. to the channel that we just created. It appends
  529. the message field created from the values of the two
  530. expressions (and cast to the appropriate types of the
  531. message fields declared for
  532. .CW qname )
  533. to the tail of the message buffer of 16 slots that belongs
  534. to channel
  535. .CW qname .
  536. By default the send statement is only executable if the target
  537. channel is non-full.
  538. (This default semantics can be changed in the verifier into
  539. one where the send statement is always executable, but the
  540. message will be lost when an attempt is made to append it to
  541. a full channel.)
  542. .LP
  543. The statement
  544. .P1
  545. qname?var1,var2
  546. .P2
  547. retrieves a message from the head of the same buffer,
  548. and stores the two expressions in variables
  549. .CW var1
  550. and
  551. .CW var2 .
  552. .LP
  553. The receive statement is executable only if the source channel
  554. is non-empty.
  555. .LP
  556. If more parameters are sent per message than were declared
  557. for the message channel, the redundant parameters are lost.
  558. If fewer parameters are sent than declared,
  559. the value of the remaining parameters is undefined.
  560. Similarly, if the receive operation tries to retrieve more
  561. parameters than available, the value of the extra parameters is
  562. undefined; if it receives fewer than the number of parameters
  563. sent, the extra information is lost.
  564. .LP
  565. An alternative, and equivalent, notation for the
  566. send and receive operations is to structure the
  567. message fields with parentheses, as follows:
  568. .P1
  569. qname!expr1(expr2,expr3)
  570. qname?var1(var2,var3)
  571. .P2
  572. In the above case, we assume that
  573. .CW qname
  574. was declared to hold messages consisting of three fields.
  575. .PP
  576. Some or all of the arguments of the receive operation
  577. can be given as constants instead of as variables:
  578. .P1
  579. qname?cons1,var2,cons2
  580. .P2
  581. In this case, an extra condition on the executability of the
  582. receive operation is that the value of all message fields
  583. specified as constants match the value of the corresponding
  584. fields in the message that is to be received.
  585. .LP
  586. Here is an example that uses some of the mechanisms introduced
  587. so far.
  588. .P1
  589. proctype A(chan q1)
  590. { chan q2;
  591. q1?q2;
  592. q2!123
  593. }
  594. .P2
  595. .P1
  596. proctype B(chan qforb)
  597. { int x;
  598. qforb?x;
  599. printf("x = %d\en", x)
  600. }
  601. .P2
  602. .P1
  603. init {
  604. chan qname = [1] of { chan };
  605. chan qforb = [1] of { int };
  606. run A(qname);
  607. run B(qforb);
  608. qname!qforb
  609. }
  610. .P2
  611. The value printed by the process of type
  612. .CW B
  613. will be
  614. .CW 123 .
  615. .LP
  616. A predefined function
  617. .CW len(qname)
  618. returns the number of messages currently
  619. stored in channel
  620. .CW qname .
  621. Two shorthands for the most common uses of this
  622. function are
  623. .CW empty(qname)
  624. and
  625. .CW full(qname) ,
  626. with the obvious connotations.
  627. .LP
  628. Since all expressions must be side-effect free,
  629. it is not valid to say:
  630. .P1
  631. (qname?var == 0)
  632. .P2
  633. or
  634. .P1
  635. (a > b && qname!123)
  636. .P2
  637. We could rewrite the second example (using an atomic sequence,
  638. as explained further in section 1.2.1):
  639. .P1
  640. atomic { (a > b && !full(qname)) -> qname!123 }
  641. .P2
  642. The meaning of the first example is ambiguous. It could mean
  643. that we want the condition to be true if the receive operation
  644. is unexecutable. In that case, we can rewrite it without
  645. side-effects as:
  646. .P1
  647. empty(qname)
  648. .P2
  649. It could also mean that we want the condition
  650. to be true when the channel does contain a message with
  651. value zero.
  652. We can specify that as follows:
  653. .P1
  654. atomic { qname?[0] -> qname?var }
  655. .P2
  656. The first statement of this atomic sequence is
  657. an expression without side-effects that
  658. evaluates to a non-zero value only if the
  659. receive operation
  660. .P1
  661. qname?0
  662. .P2
  663. would have been executable at that
  664. point (i.e., channel
  665. .CW qname
  666. contains at least one message and the oldest
  667. message stored consists of one message field
  668. equal to zero).
  669. Any receive statement can be turned into
  670. a side-effect free expression by placing square
  671. brackets around the list of all message parameters.
  672. The channel contents remain undisturbed by the
  673. evaluation of such expressions.
  674. .LP
  675. Note carefully, however, that in non-atomic sequences
  676. of two statements such as
  677. .P1
  678. !full(qname) -> qname!msgtype
  679. .P2
  680. and
  681. .P1
  682. qname?[msgtype] -> qname?msgtype
  683. .P2
  684. the second statement is not necessarily executable
  685. after the first one has been executed.
  686. There may be race conditions when access to the channels
  687. is shared between several processes.
  688. Another process can send a message to the channel
  689. just after this process determined that it was not full,
  690. or another process can steal away the
  691. message just after our process determined its presence.
  692. .LP
  693. Two other types of send and receive statements are used
  694. less frequently: sorted send and random receive.
  695. A sorted send operation is written with two, instead of one,
  696. exclamation marks, as follows:
  697. .P1
  698. qname!!msg
  699. .P2
  700. A sorted send operation will insert a message into the channel's buffer
  701. in numerical order, instead of in FIFO order.
  702. The channel contents are scanned from the first message towards the
  703. last, and the message is inserted immediately before the first message
  704. that follows it in numerical order.
  705. To determine the numerical order, all message fields are
  706. taken into account.
  707. .LP
  708. The logical counterpart of the sorted send operation
  709. is the random receive.
  710. It is written with two, instead of one, question marks:
  711. .P1
  712. qname??msg
  713. .P2
  714. A random receive operation is executable if it is executable for \f2any\f1
  715. message that is currently buffered in a message channel (instead of
  716. only for the first message in the channel).
  717. Normal send and receive operations can freely be combined with
  718. sorted send and random receive operations.
  719. .SH
  720. Rendezvous Communication
  721. .LP
  722. So far we have talked about asynchronous communication between processes
  723. via message channels, declared in statements such as
  724. .P1
  725. chan qname = [N] of { byte }
  726. .P2
  727. where
  728. .CW N
  729. is a positive constant that defines the buffer size.
  730. A logical extension is to allow for the declaration
  731. .P1
  732. chan port = [0] of { byte }
  733. .P2
  734. to define a rendezvous port.
  735. The channel size is zero, that is, the channel
  736. .CW port
  737. can pass, but cannot store, messages.
  738. Message interactions via such rendezvous ports are
  739. by definition synchronous.
  740. Consider the following example:
  741. .P1
  742. #define msgtype 33
  743. chan name = [0] of { byte, byte };
  744. active proctype A()
  745. { name!msgtype(124);
  746. name!msgtype(121)
  747. }
  748. .P2
  749. .P1
  750. active proctype B()
  751. { byte state;
  752. name?msgtype(state)
  753. }
  754. .P2
  755. Channel
  756. .CW name
  757. is a global rendezvous port.
  758. The two processes will synchronously execute their first statement:
  759. a handshake on message
  760. .CW msgtype
  761. and a transfer of the value 124 to local variable
  762. .CW state .
  763. The second statement in process
  764. .CW A
  765. will be unexecutable,
  766. because there is no matching receive operation in process
  767. .CW B .
  768. .LP
  769. If the channel
  770. .CW name
  771. is defined with a non-zero buffer capacity,
  772. the behavior is different.
  773. If the buffer size is at least 2, the process of type
  774. .CW A
  775. can complete its execution, before its peer even starts.
  776. If the buffer size is 1, the sequence of events is as follows.
  777. The process of type
  778. .CW A
  779. can complete its first send action, but it blocks on the
  780. second, because the channel is now filled to capacity.
  781. The process of type
  782. .CW B
  783. can then retrieve the first message and complete.
  784. At this point
  785. .CW A
  786. becomes executable again and completes,
  787. leaving its last message as a residual in the channel.
  788. .LP
  789. Rendezvous communication is binary: only two processes,
  790. a sender and a receiver, can be synchronized in a
  791. rendezvous handshake.
  792. .LP
  793. As the example shows, symbolic constants can be defined
  794. with preprocessor macros using
  795. .CW #define .
  796. The source text of a \*P model is translated by the standard
  797. C preprocessor.
  798. The disadvantage of defining symbolic names in this way is,
  799. however, that the \*P parser will only see the expanded text,
  800. and cannot refer to the symbolic names themselves.
  801. To prevent that, \*P also supports another way to define
  802. symbolic names, which are preserved in error reports.
  803. For instance, by including the declaration
  804. .P1
  805. mtype = { ack, msg, error, data };
  806. .P2
  807. at the top of a \*P model, the names provided between the
  808. curly braces are equivalent to integers of type
  809. .CW byte ,
  810. but known by their symbolic names to the \*V parser and the
  811. verifiers it generates.
  812. The constant values assigned start at 1, and count up.
  813. There can be only one
  814. .CW mtype
  815. declaration per model.
  816. .NH 2
  817. Control Flow
  818. .LP
  819. So far, we have seen only some of the basic statements
  820. of \*P, and the way in which they can be combined to
  821. model process behaviors.
  822. The five types of statements we have mentioned are:
  823. .CW printf ,
  824. .CW assignment ,
  825. .CW condition ,
  826. .CW send ,
  827. and
  828. .CW receive .
  829. .LP
  830. The pseudo-statement
  831. .CW skip
  832. is syntactically and semantically equivalent to the
  833. condition
  834. .CW (1)
  835. (i.e., to true), and is in fact quietly replaced with this
  836. expression by the lexical analyzer of \*V.
  837. .LP
  838. There are also five types of compound statements.
  839. .IP
  840. .RS
  841. \(bu
  842. Atomic sequences (section 1.2.1),
  843. .br
  844. \(bu
  845. Deterministic steps (section 1.2.2),
  846. .br
  847. \(bu
  848. Selections (section 1.2.3),
  849. .br
  850. \(bu
  851. Repetitions (section 1.2.4),
  852. .br
  853. \(bu
  854. Escape sequences (section 1.2.5).
  855. .RE
  856. .LP
  857. .NH 3
  858. Atomic Sequences
  859. .LP
  860. The simplest compound statement is the
  861. .CW atomic
  862. sequence:
  863. .P1
  864. atomic { /* swap the values of a and b */
  865. tmp = b;
  866. b = a;
  867. a = tmp
  868. }
  869. .P2
  870. In the example, the values of two variables
  871. .CW a
  872. and
  873. .CW b
  874. are swapped in a sequence of statement executions
  875. that is defined to be uninterruptable.
  876. That is, in the interleaving of process executions, no
  877. other process can execute statements from the moment that
  878. the first statement of this sequence begins to execute until
  879. the last one has completed.
  880. .LP
  881. It is often useful to use
  882. .CW atomic
  883. sequences to start a series of processes in such a
  884. way that none of them can start executing statements
  885. until all of them have been initialized:
  886. .P1
  887. init {
  888. atomic {
  889. run A(1,2);
  890. run B(2,3);
  891. run C(3,1)
  892. }
  893. }
  894. .P2
  895. .CW Atomic
  896. sequences may be non-deterministic.
  897. If any statement inside an
  898. .CW atomic
  899. sequence is found to be unexecutable, however,
  900. the atomic chain is broken, and another process can take over
  901. control.
  902. When the blocking statement becomes executable later,
  903. control can non-deterministically return to the process,
  904. and the atomic execution of the sequence resumes as if
  905. it had not been interrupted.
  906. .NH 3
  907. Deterministic Steps
  908. .LP
  909. Another way to define an indivisible sequence of actions
  910. is to use the
  911. .CW d_step
  912. statement.
  913. In the above case, for instance, we could also have written:
  914. .P1
  915. d_step { /* swap the values of a and b */
  916. tmp = b;
  917. b = a;
  918. a = tmp
  919. }
  920. .P2
  921. The difference between a
  922. .CW d_step
  923. sequence
  924. and an
  925. .CW atomic
  926. sequence are:
  927. .IP \(bu
  928. A
  929. .CW d_step
  930. sequence must be completely deterministic.
  931. (If non-determinism is nonetheless encountered,
  932. it is always resolved in a fixed and deterministic
  933. way: i.e., the first true guard in selection or
  934. repetition structures is always selected.)
  935. .IP \(bu
  936. No
  937. .CW goto
  938. jumps into or out of a
  939. .CW d_step
  940. sequence are permitted.
  941. .IP \(bu
  942. The execution of a
  943. .CW d_step
  944. sequence cannot be interrupted when a
  945. blocking statement is encountered.
  946. It is an error if any statement other than
  947. the first one in a
  948. .CW d_step
  949. sequence is found to be unexecutable.
  950. .IP \(bu
  951. A
  952. .CW d_step
  953. sequence is executed as one single statement.
  954. In a way, it is a mechanism for adding new types
  955. of statements to the language.
  956. .LP
  957. None of the items listed above apply to
  958. .CW atomic
  959. sequences.
  960. This means that the keyword
  961. .CW d_step
  962. can always be replaced with the keyword
  963. .CW atomic ,
  964. but the reverse is not true.
  965. (The main, perhaps the only, reason for using
  966. .CW d_step
  967. sequences is to improve the efficiency of
  968. verifications.)
  969. .NH 3
  970. Selection Structures
  971. .LP
  972. A more interesting construct is the selection structure.
  973. Using the relative values of two variables
  974. .CW a
  975. and
  976. .CW b
  977. to choose between two options, for instance, we can write:
  978. .P1
  979. if
  980. :: (a != b) -> option1
  981. :: (a == b) -> option2
  982. fi
  983. .P2
  984. The selection structure above contains two execution sequences,
  985. each preceded by a double colon.
  986. Only one sequence from the list will be executed.
  987. A sequence can be selected only if its first statement is executable.
  988. The first statement is therefore called a \f2guard\f1.
  989. .LP
  990. In the above example the guards are mutually exclusive, but they
  991. need not be.
  992. If more than one guard is executable, one of the corresponding sequences
  993. is selected nondeterministically.
  994. If all guards are unexecutable the process will block until at least
  995. one of them can be selected.
  996. There is no restriction on the type of statements that can be used
  997. as a guard: it may include sends or receives, assignments,
  998. .CW printf ,
  999. .CW skip ,
  1000. etc.
  1001. The rules of executability determine in each case what the semantics
  1002. of the complete selection structure will be.
  1003. The following example, for instance, uses receive statements
  1004. as guards in a selection.
  1005. .P1
  1006. mtype = { a, b };
  1007. chan ch = [1] of { byte };
  1008. active proctype A()
  1009. { ch!a
  1010. }
  1011. .P2
  1012. .P1
  1013. active proctype B()
  1014. { ch!b
  1015. }
  1016. .P2
  1017. .P1
  1018. active proctype C()
  1019. { if
  1020. :: ch?a
  1021. :: ch?b
  1022. fi
  1023. }
  1024. .P2
  1025. The example defines three processes and one channel.
  1026. The first option in the selection structure of the process
  1027. of type
  1028. .CW C
  1029. is executable if the channel contains
  1030. a message named
  1031. .CW a ,
  1032. where
  1033. .CW a
  1034. is a symbolic constant defined in the
  1035. .CW mtype
  1036. declaration at the start of the program.
  1037. The second option is executable if it contains a message
  1038. .CW b ,
  1039. where, similarly,
  1040. .CW b
  1041. is a symbolic constant.
  1042. Which message will be available depends on the unknown
  1043. relative speeds of the processes.
  1044. .LP
  1045. A process of the following type will either increment
  1046. or decrement the value of variable
  1047. .CW count
  1048. once.
  1049. .P1
  1050. byte count;
  1051. active proctype counter()
  1052. {
  1053. if
  1054. :: count++
  1055. :: count--
  1056. fi
  1057. }
  1058. .P2
  1059. Assignments are always executable, so the choice made
  1060. here is truly a non-deterministic one that is independent
  1061. of the initial value of the variable (zero in this case).
  1062. .NH 3
  1063. Repetition Structures
  1064. .LP
  1065. We can modify the above program as follows, to obtain
  1066. a cyclic program that randomly changes the value of
  1067. the variable up or down, by replacing the selection
  1068. structure with a repetition.
  1069. .P1
  1070. byte count;
  1071. active proctype counter()
  1072. {
  1073. do
  1074. :: count++
  1075. :: count--
  1076. :: (count == 0) -> break
  1077. od
  1078. }
  1079. .P2
  1080. Only one option can be selected for execution at a time.
  1081. After the option completes, the execution of the structure
  1082. is repeated.
  1083. The normal way to terminate the repetition structure is
  1084. with a
  1085. .CW break
  1086. statement.
  1087. In the example, the loop can be
  1088. broken only when the count reaches zero.
  1089. Note, however, that it need not terminate since the other
  1090. two options remain executable.
  1091. To force termination we could modify the program as follows.
  1092. .P1
  1093. active proctype counter()
  1094. {
  1095. do
  1096. :: (count != 0) ->
  1097. if
  1098. :: count++
  1099. :: count--
  1100. fi
  1101. :: (count == 0) -> break
  1102. od
  1103. }
  1104. .P2
  1105. A special type of statement that is useful in selection
  1106. and repetition structures is the
  1107. .CW else
  1108. statement.
  1109. An
  1110. .CW else
  1111. statement becomes executable only if no other statement
  1112. within the same process, at the same control-flow point,
  1113. is executable.
  1114. We could try to use it in two places in the above example:
  1115. .P1
  1116. active proctype counter()
  1117. {
  1118. do
  1119. :: (count != 0) ->
  1120. if
  1121. :: count++
  1122. :: count--
  1123. :: else
  1124. fi
  1125. :: else -> break
  1126. od
  1127. }
  1128. .P2
  1129. The first
  1130. .CW else ,
  1131. inside the nested selection structure, can never become
  1132. executable though, and is therefore redundant (both alternative
  1133. guards of the selection are assignments, which are always
  1134. executable).
  1135. The second usage of the
  1136. .CW else ,
  1137. however, becomes executable exactly when
  1138. .CW "!(count != 0)"
  1139. or
  1140. .CW "(count == 0)" ,
  1141. and is therefore equivalent to the latter to break from the loop.
  1142. .LP
  1143. There is also an alternative way to exit the do-loop, without
  1144. using a
  1145. .CW break
  1146. statement: the infamous
  1147. .CW goto .
  1148. This is illustrated in the following implementation of
  1149. Euclid's algorithm for finding the greatest common divisor
  1150. of two non-zero, positive numbers:
  1151. .P1
  1152. proctype Euclid(int x, y)
  1153. {
  1154. do
  1155. :: (x > y) -> x = x - y
  1156. :: (x < y) -> y = y - x
  1157. :: (x == y) -> goto done
  1158. od;
  1159. done:
  1160. skip
  1161. }
  1162. .P2
  1163. .P1
  1164. init { run Euclid(36, 12) }
  1165. .P2
  1166. The
  1167. .CW goto
  1168. in this example jumps to a label named
  1169. .CW done .
  1170. Since a label can only appear before a statement,
  1171. we have added the dummy statement
  1172. .CW skip .
  1173. Like a
  1174. .CW skip ,
  1175. a
  1176. .CW goto
  1177. statement is always executable and has no other
  1178. effect than to change the control-flow point
  1179. of the process that executes it.
  1180. .LP
  1181. As a final example, consider the following implementation of
  1182. a Dijkstra semaphore, which is implemented with the help of
  1183. a synchronous channel.
  1184. .P1
  1185. #define p 0
  1186. #define v 1
  1187. chan sema = [0] of { bit };
  1188. .P2
  1189. .P1
  1190. active proctype Dijkstra()
  1191. { byte count = 1;
  1192. do
  1193. :: (count == 1) ->
  1194. sema!p; count = 0
  1195. :: (count == 0) ->
  1196. sema?v; count = 1
  1197. od
  1198. }
  1199. .P2
  1200. .P1
  1201. active [3] proctype user()
  1202. { do
  1203. :: sema?p;
  1204. /* critical section */
  1205. sema!v;
  1206. /* non-critical section */
  1207. od
  1208. }
  1209. .P2
  1210. The semaphore guarantees that only one of the three user processes
  1211. can enter its critical section at a time.
  1212. It does not necessarily prevent the monopolization of
  1213. the access to the critical section by one of the processes.
  1214. .LP
  1215. \*P does not have a mechanism for defining functions or
  1216. procedures. Where necessary, though, these may be
  1217. modeled with the help of additional processes.
  1218. The return value of a function, for instance, can be passed
  1219. back to the calling process via global variables or messages.
  1220. The following program illustrates this by recursively
  1221. calculating the factorial of a number
  1222. .CW n .
  1223. .P1
  1224. proctype fact(int n; chan p)
  1225. { chan child = [1] of { int };
  1226. int result;
  1227. if
  1228. :: (n <= 1) -> p!1
  1229. :: (n >= 2) ->
  1230. run fact(n-1, child);
  1231. child?result;
  1232. p!n*result
  1233. fi
  1234. }
  1235. .P2
  1236. .P1
  1237. init
  1238. { chan child = [1] of { int };
  1239. int result;
  1240. run fact(7, child);
  1241. child?result;
  1242. printf("result: %d\en", result)
  1243. }
  1244. .P2
  1245. Each process creates a private channel and uses it
  1246. to communicate with its direct descendant.
  1247. There are no input statements in \*P.
  1248. The reason is that models must always be complete to
  1249. allow for logical verifications, and input statements
  1250. would leave at least the source of some information unspecified.
  1251. A way to read input
  1252. would presuppose a source of information that is not
  1253. part of the model.
  1254. .LP
  1255. We have already discussed a few special types of statement:
  1256. .CW skip ,
  1257. .CW break ,
  1258. and
  1259. .CW else .
  1260. Another statement in this class is the
  1261. .CW timeout .
  1262. The
  1263. .CW timeout
  1264. is comparable to a system level
  1265. .CW else
  1266. statement: it becomes executable if and only if no other
  1267. statement in any of the processes is executable.
  1268. .CW Timeout
  1269. is a modeling feature that provides for an escape from a
  1270. potential deadlock state.
  1271. The
  1272. .CW timeout
  1273. takes no parameters, because the types of properties we
  1274. would like to prove for \*P models must be proven independent
  1275. of all absolute and relative timing considerations.
  1276. In particular, the relative speeds of processes can never be
  1277. known with certainty in an asynchronous system.
  1278. .NH 3
  1279. Escape Sequences
  1280. .LP
  1281. The last type of compound structure to be discussed is the
  1282. .CW unless
  1283. statement.
  1284. It is used as follows:
  1285. .MT _sec5unless
  1286. .P1
  1287. { P } unless { E }
  1288. .P2
  1289. where the letters
  1290. .CW P
  1291. and
  1292. .CW E
  1293. represent arbitrary \*P fragments.
  1294. Execution of the
  1295. .CW unless
  1296. statement begins with the execution of statements from
  1297. .CW P .
  1298. Before each statement execution in
  1299. .CW P
  1300. the executability of the first statement of
  1301. .CW E
  1302. is checked, using the normal \*P semantics of executability.
  1303. Execution of statements from
  1304. .CW P
  1305. proceeds only while the first statement of
  1306. .CW E
  1307. remains unexecutable.
  1308. The first time that this `guard of the escape sequence'
  1309. is found to be executable, control changes to it,
  1310. and execution continues as defined for
  1311. .CW E .
  1312. Individual statement executions remain indivisible,
  1313. so control can only change from inside
  1314. .CW P
  1315. to the start of
  1316. .CW E
  1317. in between individual statement executions.
  1318. If the guard of the escape sequence
  1319. does not become executable during the
  1320. execution of
  1321. .CW P ,
  1322. then it is skipped entirely when
  1323. .CW P
  1324. terminates.
  1325. .LP
  1326. An example of the use of escape sequences is:
  1327. .P1
  1328. A;
  1329. do
  1330. :: b1 -> B1
  1331. :: b2 -> B2
  1332. \&...
  1333. od
  1334. unless { c -> C };
  1335. D
  1336. .P2
  1337. As shown in the example, the curly braces around the main sequence
  1338. (or the escape sequence) can be deleted if there can be no confusion
  1339. about which statements belong to those sequences.
  1340. In the example, condition
  1341. .CW c
  1342. acts as a watchdog on the repetition construct from the main sequence.
  1343. Note that this is not necessarily equivalent to the construct
  1344. .P1
  1345. A;
  1346. do
  1347. :: b1 -> B1
  1348. :: b2 -> B2
  1349. \&...
  1350. :: c -> break
  1351. od;
  1352. C; D
  1353. .P2
  1354. if
  1355. .CW B1
  1356. or
  1357. .CW B2
  1358. are non-empty.
  1359. In the first version of the example, execution of the iteration can
  1360. be interrupted at \f2any\f1 point inside each option sequence.
  1361. In the second version, execution can only be interrupted at the
  1362. start of the option sequences.
  1363. .NH 2
  1364. Correctness Properties
  1365. .LP
  1366. There are three ways to express correctness properties in \*P,
  1367. using:
  1368. .IP
  1369. .RS
  1370. .br
  1371. \(bu
  1372. Assertions (section 1.3.1),
  1373. .br
  1374. \(bu
  1375. Special labels (section 1.3.2),
  1376. .br
  1377. \(bu
  1378. .CW Never
  1379. claims (section 1.3.3).
  1380. .RE
  1381. .LP
  1382. .NH 3
  1383. Assertions
  1384. .LP
  1385. Statements of the form
  1386. .P1
  1387. assert(expression)
  1388. .P2
  1389. are always executable.
  1390. If the expression evaluates to a non-zero value (i.e., the
  1391. corresponding condition holds), the statement has no effect
  1392. when executed.
  1393. The correctness property expressed, though, is that it is
  1394. impossible for the expression to evaluate to zero (i.e., for
  1395. the condition to be false).
  1396. A failing assertion will cause execution to be aborted.
  1397. .NH 3
  1398. Special Labels
  1399. .LP
  1400. Labels in a \*P specification ordinarily serve as
  1401. targets for unconditional
  1402. .CW goto
  1403. jumps, as usual.
  1404. There are, however, also three types of labels that
  1405. have a special meaning to the verifier.
  1406. We discuss them in the next three subsections.
  1407. .NH 4
  1408. End-State Labels
  1409. .LP
  1410. When a \*P model is checked for reachable deadlock states
  1411. by the verifier, it must be able to distinguish valid \f2end state\f1s
  1412. from invalid ones.
  1413. By default, the only valid end states are those in which
  1414. every \*P process that was instantiated has reached the end of
  1415. its code.
  1416. Not all \*P processes, however, are meant to reach the
  1417. end of their code.
  1418. Some may very well linger in a known wait
  1419. state, or they may sit patiently in a loop
  1420. ready to spring into action when new input arrives.
  1421. .LP
  1422. To make it clear to the verifier that these alternate end states
  1423. are also valid, we can define special end-state labels.
  1424. We can do so, for instance, in the process type
  1425. .CW Dijkstra ,
  1426. from an earlier example:
  1427. .P1
  1428. proctype Dijkstra()
  1429. { byte count = 1;
  1430. end: do
  1431. :: (count == 1) ->
  1432. sema!p; count = 0
  1433. :: (count == 0) ->
  1434. sema?v; count = 1
  1435. od
  1436. }
  1437. .P2
  1438. The label
  1439. .CW end
  1440. defines that it is not an error if, at the end of an
  1441. execution sequence, a process of this type
  1442. has not reached its closing curly brace, but waits at the label.
  1443. Of course, such a state could still be part of a deadlock state, but
  1444. if so, it is not caused by this particular process.
  1445. .LP
  1446. There may be more than one end-state label per \*P model.
  1447. If so, all labels that occur within the same process body must
  1448. be unique.
  1449. The rule is that every label name with the prefix
  1450. .CW end
  1451. is taken to be an end-state label.
  1452. .NH 4
  1453. Progress-State Labels
  1454. .LP
  1455. In the same spirit, \*P also allows for the definition of
  1456. .CW progress
  1457. labels.
  1458. Passing a progress label during an execution is interpreted
  1459. as a good thing: the process is not just idling while
  1460. waiting for things to happen elsewhere, but is making
  1461. effective progress in its execution.
  1462. The implicit correctness property expressed here is that any
  1463. infinite execution cycle allowed by the model that does not
  1464. pass through at least one of these progress labels is a
  1465. potential starvation loop.
  1466. In the
  1467. .CW Dijkstra
  1468. example, for instance, we can label the
  1469. successful passing of a semaphore test as progress and
  1470. ask a verifier to make sure that there is no cycle elsewhere
  1471. in the system.
  1472. .P1
  1473. proctype Dijkstra()
  1474. { byte count = 1;
  1475. end: do
  1476. :: (count == 1) ->
  1477. progress: sema!p; count = 0
  1478. :: (count == 0) ->
  1479. sema?v; count = 1
  1480. od
  1481. }
  1482. .P2
  1483. If more than one state carries a progress label,
  1484. variations with a common prefix are again valid.
  1485. .NH 4
  1486. Accept-State Labels
  1487. .LP
  1488. The last type of label, the accept-state label, is used
  1489. primarily in combination with
  1490. .CW never
  1491. claims.
  1492. Briefly, by labeling a state with any label starting
  1493. with the prefix
  1494. .CW accept
  1495. we can ask the verifier to find all cycles that \f2do\f1
  1496. pass through at least one of those labels.
  1497. The implicit correctness claim is that this cannot happen.
  1498. The primary place where accept labels are used is inside
  1499. .CW never
  1500. claims.
  1501. We discuss
  1502. .CW never
  1503. claims next.
  1504. .NH 3
  1505. Never Claims
  1506. .LP
  1507. Up to this point we have talked about the specification
  1508. of correctness criteria with assertions
  1509. and with three special types of labels.
  1510. Powerful types of correctness criteria can already
  1511. be expressed with these tools, yet so far our only option is
  1512. to add them to individual
  1513. .CW proctype
  1514. declarations.
  1515. We can, for instance, express the claim ``every system state
  1516. in which property
  1517. .CW P
  1518. is true eventually leads to a system state in which property
  1519. .CW Q
  1520. is true,'' with an extra monitor process, such as:
  1521. .P1
  1522. active proctype monitor()
  1523. {
  1524. progress:
  1525. do
  1526. :: P -> Q
  1527. od
  1528. }
  1529. .P2
  1530. If we require that property
  1531. .CW P
  1532. must \f2remain\f1 true while we are waiting
  1533. .CW Q
  1534. to become true, we can try to change this to:
  1535. .P1
  1536. active proctype monitor()
  1537. {
  1538. progress:
  1539. do
  1540. :: P -> assert(P || Q)
  1541. od
  1542. }
  1543. .P2
  1544. but this does not quite do the job.
  1545. Note that we cannot make any assumptions about the
  1546. relative execution speeds of processes in a \*P model.
  1547. This means that if in the remainder of the system the
  1548. property
  1549. .CW P
  1550. becomes true, we can move to the state just before the
  1551. .CW assert ,
  1552. and wait there for an unknown amount of time (anything between
  1553. a zero delay and an infinite delay is possible here, since
  1554. no other synchronizations apply).
  1555. If
  1556. .CW Q
  1557. becomes true, we may pass the assertion, but we need not
  1558. do so.
  1559. Even if
  1560. .CW P
  1561. becomes false only \f2after\f1
  1562. .CW Q
  1563. has become true, we may still fail the assertion,
  1564. as long as there exists some later state where neither
  1565. .CW P
  1566. nor
  1567. .CW Q
  1568. is true.
  1569. This is clearly unsatisfactory, and we need another mechanism
  1570. to express these important types of liveness properties.
  1571. .SH
  1572. The Connection with Temporal Logic
  1573. .LP
  1574. A general way to express system properties of the type we
  1575. have just discussed is to use linear time temporal logic (LTL)
  1576. formulae.
  1577. Every \*P expression is automatically also a valid LTL formula.
  1578. An LTL formula can also contain the unary temporal operators □
  1579. (pronounced always), ◊ (pronounced eventually), and
  1580. two binary temporal operators
  1581. .CW U
  1582. (pronounced weak until) and
  1583. .BI U
  1584. (pronounced strong until).
  1585. .LP
  1586. Where the value of a \*P expression without temporal operators can be
  1587. defined uniquely for individual system states, without further context,
  1588. the truth value of an LTL formula is defined for sequences of states:
  1589. specifically, it is defined for the first state of a given infinite
  1590. sequence of system states (a trace).
  1591. Given, for instance, the sequence of system states:
  1592. .P1
  1593. s0;s1;s2;...
  1594. .P2
  1595. the LTL formula
  1596. .CW pUq ,
  1597. with
  1598. .CW p
  1599. and
  1600. .CW q
  1601. standard \*P expressions, is true for
  1602. .CW s0
  1603. either if
  1604. .CW q
  1605. is true in
  1606. .CW s0 ,
  1607. or if
  1608. .CW p
  1609. is true in
  1610. .CW s0
  1611. and
  1612. .CW pUq
  1613. holds for the remainder of the sequence after
  1614. .CW s0 .
  1615. .LP
  1616. Informally,
  1617. .CW pUq
  1618. says that
  1619. .CW p
  1620. is required to hold at least until
  1621. .CW q
  1622. becomes true.
  1623. If, instead, we would write \f(CWp\f(BIU\f(CWq\f1,
  1624. then we also require that there exists at least
  1625. one state in the sequence where
  1626. .CW q
  1627. does indeed become true.
  1628. .LP
  1629. The temporal operators □ and ◊
  1630. can be defined in terms of the strong until operator
  1631. .BI U ,
  1632. as follows.
  1633. .P1
  1634. □ p = !◊ !p = !(true \f(BIU\f(CW !p)
  1635. .P2
  1636. Informally, □
  1637. .CW p
  1638. says that property
  1639. .CW p
  1640. must hold in all states of a trace, and ◊
  1641. .CW p
  1642. says that
  1643. .CW p
  1644. holds in at least one state of the trace.
  1645. .LP
  1646. To express our original example requirement: ``every system state
  1647. in which property
  1648. .CW P
  1649. is true eventually leads to a system state in which property
  1650. .CW Q
  1651. is true,''
  1652. we can write the LTL formula:
  1653. .P1
  1654. □ (P -> ◊ Q)
  1655. .P2
  1656. where the logical implication symbol
  1657. .CW ->
  1658. is defined in the usual way as
  1659. .P1
  1660. P => Q means !P || Q
  1661. .P2
  1662. .SH
  1663. Mapping LTL Formulae onto Never Claims
  1664. .LP
  1665. \*P does not include syntax for specifying LTL formulae
  1666. directly, but it relies on the fact that every such
  1667. formula can be translated into a special type of
  1668. automaton, known as a Büchi automaton.
  1669. In the syntax of \*P this automaton is called a
  1670. .CW never
  1671. claim.
  1672. If you don't care too much about the details of
  1673. .CW never
  1674. claims, you can skip the remainder of this section and
  1675. simple remember that \*V can convert any LTL formula
  1676. automatically into the proper never claim syntax with
  1677. the command:
  1678. .P1
  1679. spin -f "...formula..."
  1680. .P2
  1681. Here are the details.
  1682. The syntax of a never claim is:
  1683. .P1
  1684. never {
  1685. \&...
  1686. }
  1687. .P2
  1688. where the dots can contain any \*P fragment, including
  1689. arbitrary repetition, selection, unless constructs,
  1690. jumps, etc.
  1691. .LP
  1692. There is an important difference in semantics between a
  1693. .CW proctype
  1694. declaration and a
  1695. .CW never
  1696. claim.
  1697. Every statement inside a
  1698. .CW never
  1699. claim is interpreted as a proposition, i.e., a condition.
  1700. A
  1701. .CW never
  1702. claim should therefore only contain expressions and never
  1703. statements that can have side-effects (assignments, sends or
  1704. receives, run-statements, etc.)
  1705. .LP
  1706. .CW Never
  1707. claims are used to express behaviors that are considered
  1708. undesirable or illegal.
  1709. We say that a
  1710. .CW never
  1711. claim is `matched' if the undesirable behavior can be realized,
  1712. contrary to the claim, and thus the correctness requirement violated.
  1713. The claims are evaluated over system executions, that is, the
  1714. propositions that are listed in the claim are evaluated over the
  1715. traces from the remainder of the system.
  1716. The claim, therefore, should not alter that behavior: it merely
  1717. monitors it.
  1718. Every time that the system reaches a new state, by asynchronously
  1719. executing statements from the model, the claim will evaluate the
  1720. appropriate propositions to determine if a counter-example can
  1721. be constructed to the implicit LTL formula that is specified.
  1722. .LP
  1723. Since LTL formulae are only defined for infinite executions,
  1724. the behavior of a
  1725. .CW never
  1726. claim can only be matched by an infinite system execution.
  1727. This by itself would restrict us to the use of progress labels
  1728. and accept labels as the only means we have discussed so far
  1729. for expressing properties of infinite behaviors.
  1730. To conform to standard omega automata theory, the behaviors of
  1731. .CW never
  1732. claims are expressed exclusively with
  1733. .CW accept
  1734. labels (never with
  1735. .CW progress
  1736. labels).
  1737. To match a claim, therefore, an infinite sequence of true propositions
  1738. must exist, at least one of which is labeled with an
  1739. .CW accept
  1740. label (inside the never claim).
  1741. .LP
  1742. Since \*P models can also express terminating system behaviors,
  1743. we have to define the semantics of the
  1744. .CW never
  1745. claims also for those behaviors.
  1746. To facilitate this, it is defined that a
  1747. .CW never
  1748. claim can also be matched when it reaches its closing curly brace
  1749. (i.e., when it appears to terminate).
  1750. This semantics is based on what is usually referred to as a `stuttering
  1751. semantics.'
  1752. With stuttering semantics, any terminating execution can be extended
  1753. into an equivalent infinite execution (for the purposes of evaluating
  1754. LTL properties) by repeating (stuttering) the final state infinitely often.
  1755. As a syntactical convenience, the final state of a
  1756. .CW never
  1757. claim is defined to be accepting, i.e., it could be replaced with
  1758. the explicit repetition construct:
  1759. .P1
  1760. accept: do :: skip od
  1761. .P2
  1762. Every process behavior, similarly, is (for the purposes of evaluating the
  1763. .CW never
  1764. claims) thought to be extended with a dummy self-loop on all final states:
  1765. .P1
  1766. do :: skip od
  1767. .P2
  1768. (Note the
  1769. .CW accept
  1770. labels only occur in the
  1771. .CW never
  1772. claim, not in the system.)
  1773. .SH
  1774. The Semantics of a Never Claim
  1775. .LP
  1776. .CW Never
  1777. claims are probably the hardest part of the language to understand,
  1778. so it is worth spending a few extra words on them.
  1779. On an initial reading, feel free to skip the remainder of this
  1780. section.
  1781. .LP
  1782. The difference between a
  1783. .CW never
  1784. claim and the remainder of a \*P system can be explained
  1785. as follows.
  1786. A \*P model defines an asynchronous interleaving product of the
  1787. behaviors of individual processes.
  1788. Given an arbitrary system state, its successor states are
  1789. conceptually obtained in two steps.
  1790. In a first step, all the executable statements in the
  1791. individual processes are identified.
  1792. In a second step, each one of these statements is executed,
  1793. each one producing one potential successor for the current state.
  1794. The complete system behavior is thus defined recursively and
  1795. represents all possible interleavings of the individual process behaviors.
  1796. It is this asynchronous product machine that we call the `global
  1797. system behavior'.
  1798. .LP
  1799. The addition of a
  1800. .CW never
  1801. claim defines a \f2synchronous\f1 product of the global system behavior
  1802. with the behavior expressed in the claim.
  1803. This synchronous product can be thought of as the construction of a
  1804. new global state machine, in which every state is defined as a pair
  1805. .CW (s,n)
  1806. with
  1807. .CW s
  1808. a state from the global system (the asynchronous product of processes), and
  1809. .CW n
  1810. a state from the claim.
  1811. Every transition in the new global machine is similarly defined by a pair
  1812. of transitions, with the first element a statement from the system, and the
  1813. second a proposition from the claim.
  1814. In other words, every transition in this final synchronous product is
  1815. defined as a joint transition of the system and the claim.
  1816. Of course, that transition can only occur if the proposition from the
  1817. second half of the transition pair evaluates to true in the current state
  1818. of the system (the first half of the state pair).
  1819. .SH
  1820. Examples
  1821. .LP
  1822. To manually translate an LTL formula into a
  1823. .CW never
  1824. claim (e.g. foregoing the builtin translation that \*V
  1825. offers), we must carefully consider whether the
  1826. formula expresses a positive or a negative property.
  1827. A positive property expresses a good behavior that we
  1828. would like our system to have.
  1829. A negative property expresses a bad behavior that we
  1830. claim the system does not have.
  1831. A
  1832. .CW never
  1833. claim can express only negative claims, not positive ones.
  1834. Fortunately, the two are exchangeable: if we want to express
  1835. that a good behavior is unavoidable, we can formalize all
  1836. ways in which the good behavior could be violated, and express
  1837. that in the
  1838. .CW never
  1839. claim.
  1840. .LP
  1841. Suppose that the LTL formula ◊□
  1842. .CW p ,
  1843. with
  1844. .CW p
  1845. a \*P expression, expresses a negative claim
  1846. (i.e., it is considered a correctness violation if
  1847. there exists any execution sequence in which
  1848. .CW p
  1849. can eventually remain true infinitely long).
  1850. This can be written in a
  1851. .CW never
  1852. claim as:
  1853. .P1
  1854. never { /* <>[]p */
  1855. do
  1856. :: skip /* after an arbitrarily long prefix */
  1857. :: p -> break /* p becomes true */
  1858. od;
  1859. accept: do
  1860. :: p /* and remains true forever after */
  1861. od
  1862. }
  1863. .P2
  1864. Note that in this case the claim does not terminate, and
  1865. also does not necessarily match all system behaviors.
  1866. It is sufficient if it precisely captures all violations
  1867. of our correctness requirement, and no more.
  1868. .LP
  1869. If the LTL formula expressed a positive property, we first
  1870. have to invert it to the corresponding negative property
  1871. .CW ◊!p
  1872. and translate that into a
  1873. .CW never
  1874. claim.
  1875. The requirement now says that it is a violation if
  1876. .CW p
  1877. does not hold infinitely long.
  1878. .P1
  1879. never { /* <>!p*/
  1880. do
  1881. :: skip
  1882. :: !p -> break
  1883. od
  1884. }
  1885. .P2
  1886. We have used the implicit match of a claim upon reaching the
  1887. closing terminating brace.
  1888. Since the first violation of the property suffices to disprove
  1889. it, we could also have written:
  1890. .P1
  1891. never { /* <>!p*/
  1892. do
  1893. :: p
  1894. :: !p -> break
  1895. od
  1896. }
  1897. .P2
  1898. or, if we abandon the connection with LTL for a moment,
  1899. even more tersely as:
  1900. .P1
  1901. never { do :: assert(p) od }
  1902. .P2
  1903. Suppose we wish to express that it is a violation of our
  1904. correctness requirements if there exists any execution in
  1905. the system where
  1906. .CW "□ (p -> ◊ q)"
  1907. is violated (i.e., the negation of this formula is satisfied).
  1908. The following
  1909. .CW never
  1910. claim expresses that property:
  1911. .P1
  1912. never {
  1913. do
  1914. :: skip
  1915. :: p && !q -> break
  1916. od;
  1917. accept:
  1918. do
  1919. :: !q
  1920. od
  1921. }
  1922. .P2
  1923. Note that using
  1924. .CW "(!p || q)"
  1925. instead of
  1926. .CW skip
  1927. in the first repetition construct would imply a check for just
  1928. the first occurrence of proposition
  1929. .CW p
  1930. becoming true in the execution sequence, while
  1931. .CW q
  1932. is false.
  1933. The above formalization checks for all occurrences, anywhere in a trace.
  1934. .LP
  1935. Finally, consider a formalization of the LTL property
  1936. .CW "□ (p -> (q U r))" .
  1937. The corresponding claim is:
  1938. .P1
  1939. never {
  1940. do
  1941. :: skip /* to match any occurrence */
  1942. :: p && q && !r -> break
  1943. :: p && !q && !r -> goto error
  1944. od;
  1945. do
  1946. :: q && !r
  1947. :: !q && !r -> break
  1948. od;
  1949. error: skip
  1950. }
  1951. .P2
  1952. Note again the use of
  1953. .CW skip
  1954. instead of
  1955. .CW "(!p || r)"
  1956. to avoid matching just the first occurrence of
  1957. .CW "(p && !r)"
  1958. in a trace.
  1959. .NH 2
  1960. Predefined Variables and Functions
  1961. .LP
  1962. The following predefined variables and functions
  1963. can be especially useful in
  1964. .CW never
  1965. claims.
  1966. .LP
  1967. The predefined variables are:
  1968. .CW _pid
  1969. and
  1970. .CW _last .
  1971. .LP
  1972. .CW _pid
  1973. is a predefined local variable in each process
  1974. that holds the unique instantiation number for
  1975. that process.
  1976. It is always a non-negative number.
  1977. .LP
  1978. .CW _last
  1979. is a predefined global variable that always holds the
  1980. instantiation number of the process that performed the last
  1981. step in the current execution sequence.
  1982. Its value is not part of the system state unless it is
  1983. explicitly used in a specification.
  1984. .P1
  1985. never {
  1986. /* it is not possible for the process with pid=1
  1987. * to execute precisely every other step forever
  1988. */
  1989. accept:
  1990. do
  1991. :: _last != 1 -> _last == 1
  1992. od
  1993. }
  1994. .P2
  1995. The initial value of
  1996. .CW _last
  1997. is zero.
  1998. .LP
  1999. Three predefined functions are specifically intended to be used in
  2000. .CW never
  2001. claims, and may not be used elsewhere in a model:
  2002. .CW pc_value(pid) ,
  2003. .CW enabled(pid) ,
  2004. .CW procname[pid]@label .
  2005. .LP
  2006. The function
  2007. .CW pc_value(pid)
  2008. returns the current control state
  2009. of the process with instantiation number
  2010. .CW pid ,
  2011. or zero if no such process exists.
  2012. .LP
  2013. Example:
  2014. .P1
  2015. never {
  2016. /* Whimsical use: claim that it is impossible
  2017. * for process 1 to remain in the same control
  2018. * state as process 2, or one with smaller value.
  2019. */
  2020. accept: do
  2021. :: pc_value(1) <= pc_value(2)
  2022. od
  2023. }
  2024. .P2
  2025. The function
  2026. .CW enabled(pid)
  2027. tells whether the process with instantiation number
  2028. .CW pid
  2029. has an executable statement that it can execute next.
  2030. .LP
  2031. Example:
  2032. .P1
  2033. never {
  2034. /* it is not possible for the process with pid=1
  2035. * to remain enabled without ever executing
  2036. */
  2037. accept:
  2038. do
  2039. :: _last != 1 && enabled(1)
  2040. od
  2041. }
  2042. .P2
  2043. The last function
  2044. .CW procname[pid]@label
  2045. tells whether the process with instantiation number
  2046. .CW pid
  2047. is currently in the state labeled with
  2048. .CW label
  2049. in
  2050. .CW "proctype procname" .
  2051. It is an error if the process referred to is not an instantiation
  2052. of that proctype.
  2053. .NH 1
  2054. Verifications with \*V
  2055. .LP
  2056. The easiest way to use \*V is probably on a Windows terminal
  2057. with the Tcl/Tk implementation of \s-1XSPIN\s0.
  2058. All functionality of \*V, however, is accessible from
  2059. any plain ASCII terminal, and there is something to be
  2060. said for directly interacting with the tool itself.
  2061. .LP
  2062. The description in this paper gives a short walk-through of
  2063. a common mode of operation in using the verifier.
  2064. A more tutorial style description of the verification
  2065. process can be found in [Ho93].
  2066. More detail on the verification of large systems with the
  2067. help of \*V's supertrace (bitstate) verification algorithm
  2068. can be found in [Ho95].
  2069. .IP
  2070. .RS
  2071. .br
  2072. \(bu
  2073. Random and interactive simulations (section 2.1),
  2074. .br
  2075. \(bu
  2076. Generating a verifier (section 2.2),
  2077. .br
  2078. \(bu
  2079. Compilation for different types of searches (section 2.3),
  2080. .br
  2081. \(bu
  2082. Performing the verification (section 2.4),
  2083. .br
  2084. \(bu
  2085. Inspecting error traces produced by the verifier (section 2.5),
  2086. .br
  2087. \(bu
  2088. Exploiting partial order reductions (section 2.6).
  2089. .RE
  2090. .LP
  2091. .NH 2
  2092. Random and Interactive Simulations
  2093. .LP
  2094. Given a model in \*P, say stored in a file called
  2095. .CW spec ,
  2096. the easiest mode of operation is to perform a random simulation.
  2097. For instance,
  2098. .P1
  2099. spin -p spec
  2100. .P2
  2101. tells \*V to perform a random simulation, while printing the
  2102. process moves selected for execution at each step (by default
  2103. nothing is printed, other than explicit
  2104. .CW printf
  2105. statements that appear in the model itself).
  2106. A range of options exists to make the traces more verbose,
  2107. e.g., by adding printouts of local variables (add option
  2108. .CW -l ),
  2109. global variables (add option
  2110. .CW -g ),
  2111. send statements (add option
  2112. .CW -s ),
  2113. or receive statements (add option
  2114. .CW -r ).
  2115. Use option
  2116. .CW -n N
  2117. (with N any number) to fix the seed on \*V's internal
  2118. random number generator, and thus make the simulation runs
  2119. reproducible.
  2120. By default the current time is used to seed the random number
  2121. generator.
  2122. For instance:
  2123. .P1
  2124. spin -p -l -g -r -s -n1 spec
  2125. .P2
  2126. .LP
  2127. If you don't like the system randomly resolving non-deterministic
  2128. choices for you, you can select an interactive simulation:
  2129. .P1
  2130. spin -i -p spec
  2131. .P2
  2132. In this case you will be offered a menu with choices each time
  2133. the execution could proceed in more than one way.
  2134. .LP
  2135. Simulations, of course, are intended primarily for the
  2136. debugging of a model. They cannot prove anything about it.
  2137. Assertions will be evaluated during simulation runs, and
  2138. any violations that result will be reported, but none of
  2139. the other correctness requirements can be checked in this way.
  2140. .NH 2
  2141. Generating the Verifier
  2142. .LP
  2143. A model-specific verifier is generated as follows:
  2144. .P1
  2145. spin -a spec
  2146. .P2
  2147. This generates a C program in a number of files (with names
  2148. starting with
  2149. .CW pan ).
  2150. .NH 2
  2151. Compiling the Verifier
  2152. .LP
  2153. At this point it is good to know the physical limitations of
  2154. the computer system that you will run the verification on.
  2155. If you know how much physical (not virtual) memory your system
  2156. has, you can take advantage of that.
  2157. Initially, you can simply compile the verifier for a straight
  2158. exhaustive verification run (constituting the strongest type
  2159. of proof if it can be completed).
  2160. Compile as follows.
  2161. .P1
  2162. \*C -o pan pan.c # standard exhaustive search
  2163. .P2
  2164. If you know a memory bound that you want to restrict the run to
  2165. (e.g., to avoid paging), find the nearest power of 2 (e.g., 23
  2166. for the bound $2 sup 23# bytes) and compile as follows.
  2167. .P1
  2168. \*C '-DMEMCNT=23' -o pan pan.c
  2169. .P2
  2170. or equivalently in terms of MegaBytes:
  2171. .P1
  2172. \*C '-DMEMLIM=8' -o pan pan.c
  2173. .P2
  2174. If the verifier runs out of memory before completing its task,
  2175. you can decide to increase the bound or to switch to a frugal
  2176. supertrace verification. In the latter case, compile as follows.
  2177. .P1
  2178. \*C -DBITSTATE -o pan pan.c
  2179. .P2
  2180. .NH 2
  2181. Performing the Verification
  2182. .LP
  2183. There are three specific decisions to make to
  2184. perform verifications optimally: estimating the
  2185. size of the reachable state space (section 2.4.1),
  2186. estimating the maximum length of a unique execution
  2187. sequence (2.4.2), and selecting the type of correctness
  2188. property (2.4.3).
  2189. No great harm is done if the estimates from the first two
  2190. steps are off. The feedback from the verifier usually provides
  2191. enough clues to determine quickly what the optimal settings
  2192. for peak performance should be.
  2193. .NH 3
  2194. Reachable States
  2195. .LP
  2196. For a standard exhaustive run, you can override the default choice
  2197. for the size for the hash table ($2 sup 18# slots) with option
  2198. .CW -w .
  2199. For instance,
  2200. .P1
  2201. pan -w23
  2202. .P2
  2203. selects $2 sup 23# slots.
  2204. The hash table size should optimally be roughly equal to the number of
  2205. reachable states you expect (within say a factor of two or three).
  2206. Too large a number merely wastes memory, too low a number wastes
  2207. CPU time, but neither can affect the correctness of the result.
  2208. .sp
  2209. For a supertrace run, the hash table \f2is\f1 the memory arena, and
  2210. you can override the default of $2 sup 22# bits with any other number.
  2211. Set it to the maximum size of physical memory you can grab without
  2212. making the system page, again within a factor of say two or three.
  2213. Use, for instance
  2214. .CW -w23
  2215. if you expect 8 million reachable states and have access to at least
  2216. 8 million ($2 sup 23#) bits of memory (i.e., $2 sup 20# or 1 Megabyte of RAM).
  2217. .NH 3
  2218. Search Depth
  2219. .LP
  2220. By default the analyzers have a search depth restriction of 10,000 steps.
  2221. If this isn't enough, the search will truncate at 9,999 steps (watch for
  2222. it in the printout).
  2223. Define a different search depth with the -m flag.
  2224. .P1
  2225. pan -m100000
  2226. .P2
  2227. If you exceed also this limit, it is probably good to take some
  2228. time to consider if the model you have specified is indeed finite.
  2229. Check, for instance, if no unbounded number of processes is created.
  2230. If satisfied that the model is finite, increase the search depth at
  2231. least as far as is required to avoid truncation completely.
  2232. .LP
  2233. If you find a particularly nasty error that takes a large number of steps
  2234. to hit, you may also set lower search depths to find the shortest variant
  2235. of an error sequence.
  2236. .P1
  2237. pan -m40
  2238. .P2
  2239. Go up or down by powers of two until you find the place where the
  2240. error first appears or disappears and then home in on the first
  2241. depth where the error becomes apparent, and use the error trail of
  2242. that verification run for guided simulation.
  2243. .sp
  2244. Note that if a run with a given search depth fails to find
  2245. an error, this does not necessarily mean that no violation of a
  2246. correctness requirement is possible within that number of steps.
  2247. The verifier performs its search for errors by using a standard
  2248. depth-first graph search. If the search is truncated at N steps,
  2249. and a state at level N-1 happens to be reachable also within fewer
  2250. steps from the initial state, the second time it is reached it
  2251. will not be explored again, and thus neither will its successors.
  2252. Those successors may contain errors states that are reachable within
  2253. N steps from the initial state.
  2254. Normally, the verification should be run in such a way that no
  2255. execution paths can be truncated, but to force the complete exploration
  2256. of also truncated searches one can override the defaults with a compile-time
  2257. flag
  2258. .CW -DREACH .
  2259. When the verifier is compiled with that additional directive, the depth at
  2260. which each state is visited is remembered, and a state is now considered
  2261. unvisited if it is revisited via a shorter path later in the search.
  2262. (This option cannot be used with a supertrace search.)
  2263. .NH 3
  2264. Liveness or Safety Verification
  2265. .LP
  2266. For the last, and perhaps the most critical, runtime decision:
  2267. it must be decided if the system is to be checked for safety
  2268. violations or for liveness violations.
  2269. .P1
  2270. pan -l # search for non-progress cycles
  2271. pan -a # search for acceptance cycles
  2272. .P2
  2273. (In the first case, though, you must compile pan.c with -DNP as an
  2274. additional directive. If you forget, the executable will remind you.)
  2275. If you don't use either of the above two options, the default types of
  2276. correctness properties are checked (assertion violations,
  2277. completeness, race conditions, etc.).
  2278. Note that the use of a
  2279. .CW never
  2280. claim that contains
  2281. .CW accept
  2282. labels requires the use of the
  2283. .CW -a
  2284. flag for complete verification.
  2285. .LP
  2286. Adding option
  2287. .CW -f
  2288. restricts the search for liveness properties further under
  2289. a standard \f2weak fairness\f1 constraint:
  2290. .P1
  2291. pan -f -l # search for weakly fair non-progress cycles
  2292. pan -f -a # search for weakly fair acceptance cycles
  2293. .P2
  2294. With this constraint, each process is required to appear
  2295. infinitely often in the infinite trace that constitutes
  2296. the violation of a liveness property (e.g., a non-progress cycle
  2297. or an acceptance cycle), unless it is permanently blocked
  2298. (i.e., has no executable statements after a certain point in
  2299. the trace is reached).
  2300. Adding the fairness constraint increases the time complexity
  2301. of the verification by a factor that is linear in the number
  2302. of active processes.
  2303. .LP
  2304. By default, the verifier will report on unreachable code in
  2305. the model only when a verification run is successfully
  2306. completed.
  2307. This default behavior can be turned off with the runtime option
  2308. .CW -n ,
  2309. as in:
  2310. .P1
  2311. pan -n -f -a
  2312. .P2
  2313. (The order in which the options such as these are listed is
  2314. always irrelevant.)
  2315. A brief explanation of these and other runtime options can
  2316. be determined by typing:
  2317. .P1
  2318. pan --
  2319. .P2
  2320. .NH 2
  2321. Inspecting Error Traces
  2322. .LP
  2323. If the verification run reports an error,
  2324. any error, \*V dumps an error trail into a file named
  2325. .CW spec.trail ,
  2326. where
  2327. .CW spec
  2328. is the name of your original \*P file.
  2329. To inspect the trail, and determine the cause of the error,
  2330. you must use the guided simulation option.
  2331. For instance:
  2332. .P1
  2333. spin -t -c spec
  2334. .P2
  2335. gives you a summary of message exchanges in the trail, or
  2336. .P1
  2337. spin -t -p spec
  2338. .P2
  2339. gives a printout of every single step executed.
  2340. Add as many extra or different options as you need to pin down the error:
  2341. .P1
  2342. spin -t -r -s -l -g spec
  2343. .P2
  2344. Make sure the file
  2345. .CW spec
  2346. didn't change since you generated the analyzer from it.
  2347. .sp
  2348. If you find non-progress cycles, add or delete progress labels
  2349. and repeat the verification until you are content that you have found what
  2350. you were looking for.
  2351. .sp
  2352. If you are not interested in the first error reported,
  2353. use pan option
  2354. .CW -c
  2355. to report on specific others:
  2356. .P1
  2357. pan -c3
  2358. .P2
  2359. ignores the first two errors and reports on the third one that
  2360. is discovered.
  2361. If you just want to count all errors and not see them, use
  2362. .P1
  2363. pan -c0
  2364. .P2
  2365. .SH
  2366. State Assignments
  2367. .LP
  2368. Internally, the verifiers produced by \*V deal with a formalization of
  2369. a \*P model in terms of extended finite state machines.
  2370. \*V therefore assigns state numbers to all statements in the model.
  2371. The state numbers are listed in all the relevant output to make it
  2372. completely unambiguous (source line references unfortunately do not
  2373. have that property).
  2374. To confirm the precise state assignments, there is a runtime option
  2375. to the analyzer generated:
  2376. .P1
  2377. pan -d # print state machines
  2378. .P2
  2379. which will print out a table with all state assignments for each
  2380. .CW proctype
  2381. in the model.
  2382. .NH 2
  2383. Exploiting Partial Order Reductions
  2384. .LP
  2385. The search algorithm used by \*V is optimized
  2386. according to the rules of a partial order theory explained in [HoPe94].
  2387. The effect of the reduction, however, can be increased considerably if the verifier
  2388. has extra information about the access of processes to global
  2389. message channels.
  2390. For this purpose, there are two keywords in the language that
  2391. allow one to assert that specific channels are used exclusively
  2392. by specific processes.
  2393. For example, the assertions
  2394. .P1
  2395. xr q1;
  2396. xs q2;
  2397. .P2
  2398. claim that the process that executes them is the \f2only\f1 process
  2399. that will receive messages from channel
  2400. .CW q1 ,
  2401. and the \f2only\f1 process that will send messages to channel
  2402. .CW q2 .
  2403. .LP
  2404. If an exclusive usage assertion turns out to be invalid, the
  2405. verifier will be able to detect this, and report it as a violation
  2406. of an implicit correctness requirement.
  2407. .LP
  2408. Every read or write access to a message channel can introduce
  2409. new dependencies that may diminish the maximum effect of the
  2410. partial order reduction strategies.
  2411. If, for instance, a process uses the
  2412. .CW len
  2413. function to check the number of messages stored in a channel,
  2414. this counts as a read access, which can in some cases invalidate
  2415. an exclusive access pattern that might otherwise exist.
  2416. There are two special functions that can be used to poll the
  2417. size of a channel in a safe way that is compatible with the
  2418. reduction strategy.
  2419. .LP
  2420. The expression
  2421. .CW nfull(qname)
  2422. returns true if channel
  2423. .CW qname
  2424. is not full, and
  2425. .CW nempty(qname)
  2426. returns true if channel
  2427. .CW qname
  2428. contains at least one message.
  2429. Note that the parser will not recognize the free form expressions
  2430. .CW !full(qname)
  2431. and
  2432. .CW !empty(qname)
  2433. as equally safe, and it will forbid constructions such as
  2434. .CW !nfull(qname)
  2435. or
  2436. .CW !nempty(qname) .
  2437. More detail on this aspect of the reduction algorithms can be
  2438. found in [HoPe94].
  2439. .SH
  2440. Keywords
  2441. .LP
  2442. For reference, the following table contains all the keywords,
  2443. predefined functions, predefined variables, and
  2444. special label-prefixes of the language \*P,
  2445. and refers to the section of this paper in
  2446. which they were discussed.
  2447. .KS
  2448. .TS
  2449. center;
  2450. l l l l.
  2451. _last (1.4) _pid (1.1.1) accept (1.3.2) active (1.1.1)
  2452. assert (1.3.1) atomic (1.2.1) bit (1.1.2) bool (1.1.2)
  2453. break (1.2.4) byte (1.1.2) chan (1.1.3) d_step (1.2.2)
  2454. do (1.2.4) else (1.2.4) empty (1.1.3) enabled (1.4)
  2455. end (1.3.2) fi (1.2.3) full (1.1.3) goto (1.2.2)
  2456. hidden (not discussed) if (1.2.3) init (1.1.1) int (1.1.2)
  2457. len (1.1.3) mtype (1.1.3) nempty (2.6) never (1.3.3)
  2458. nfull (2.6) od (1.2.4) of (1.1.3) pc_value (1.4)
  2459. printf (1.1.1) proctype (1.1.1) progress (1.3.2) run (1.1.1)
  2460. short (1.1.2) skip (1.2) timeout (1.2.4) typedef (1.1.2)
  2461. unless (1.2.5) xr (2.6) xs (2.6)
  2462. .TE
  2463. .KE
  2464. .SH
  2465. References
  2466. .LP
  2467. [Ho91]
  2468. G.J. Holzmann,
  2469. .I
  2470. Design and Validation of Computer Protocols,
  2471. .R
  2472. Prentice Hall, 1991.
  2473. .LP
  2474. [Ho93]
  2475. G.J. Holzmann, ``Tutorial: Design and Validation of Protocols,''
  2476. .I
  2477. Computer Networks and ISDN Systems,
  2478. .R
  2479. 1993, Vol. 25, No. 9, pp. 981-1017.
  2480. .LP
  2481. [HoPe94]
  2482. G.J. Holzmann and D.A. Peled, ``An improvement in
  2483. formal verification,''
  2484. .I
  2485. Proc. 7th Int. Conf. on Formal Description Techniques,
  2486. .R
  2487. FORTE94, Berne, Switzerland. October 1994.
  2488. .LP
  2489. [Ho95]
  2490. G.J. Holzmann, ``An Analysis of Bitstate Hashing,''
  2491. technical report 2/95, available from author.
  2492. .LP
  2493. [HS99]
  2494. G.J. Holzmann, ``Software model checking: extracting
  2495. verification models from source code,''
  2496. .I
  2497. Proc. Formal Methods in Software Engineering and Distributed
  2498. Systems,
  2499. .R
  2500. PSTV/FORTE99, Beijng, China, Oct. 1999, Kluwer,pp. 481-497.