1
0

spin.ms 66 KB

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