Changes between Version 28 and Version 29 of Language
- Timestamp:
- 05/20/23 10:11:54 (3 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
Language
v28 v29 13 13 === The integer type 14 14 15 There is one integer type, corresponding to the mathematical integers. Currently, all of the C integer types `int`, `long`, `unsigned int`, `short`, etc., are mapped to the CIVL integer type. [This is expected to change.] 15 There is one integer type, corresponding to the mathematical integers. 16 Currently, all of the C integer types `int`, `long`, `unsigned int`, `short`, etc., are mapped to the CIVL integer type. 17 [This is expected to change.] 16 18 17 19 === The real type … … 184 186 }}} 185 187 186 187 188 === This scope: the `$here` scope expression 188 189 Expression of type `$scope`, evaluating to the dynamic scope in which the evaluation takes place. … … 194 195 Constant of type `$scope`, the root dynamic scope. 195 196 196 === Range literals 197 === Range literals: `lo .. hi` 197 198 198 199 An expression of the form `lo .. hi` where `lo` and `hi` are integer expressions, represents the range consisting of the integers `lo`, `lo` + 1, ..., `hi` (in that order). … … 242 243 === This process: `$self` 243 244 244 This expression of `$proc` type returns a reference to the process which is evaluating this expression. It provides a way for code to obtain the identity of the process executing the code. 245 This expression of `$proc` type returns a reference to the process which is evaluating this expression. 246 It provides a way for code to obtain the identity of the process executing the code. 245 247 246 248 === Spawning a new process: `$spawn` 247 249 248 A spawn expression is an expression with side-effects. It spawns a new process and returns a reference to the new process, i.e., an object of type $proc. The syntax is the same as a procedure invocation with the keyword `$spawn` inserted in front: 250 A spawn expression is an expression with side-effects. 251 It spawns a new process and returns a reference to the new process, i.e., an object of type $proc. 252 The syntax is the same as a procedure invocation with the keyword `$spawn` inserted in front: 249 253 {{{ 250 254 $spawn f(expr1, ..., exprn) … … 276 280 The process may not necessarily enter the atomic block as soon as these conditions hold, because some other enabled process may be scheduled first. 277 281 In fact, some other process may obtain the atomic lock. 278 But if the enabling conditions hold and this process is scheduled, it will obtain the atomic lock and begin executing the statements of the atomic block without other processes executing. 282 But if the enabling conditions hold and this process is scheduled, it will obtain the atomic lock and begin executing the statements 283 of the atomic block without other processes executing. 279 284 Upon reaching the end of the atomic block, the process releases the atomic lock and exits the block. 280 285 281 286 There is an exception to atomicity: if the process inside the atomic block executes a `$yield` statement, it releases the atomic lock. 282 287 This allows other processes to execute, and even obtain the lock. 283 At any point at which the atomic lock is free and the first statement following the `$yield` is enabled, the original process may re-obtain the atomic lock and continue executing its block atomically. 288 At any point at which the atomic lock is free and the first statement following the `$yield` is enabled, the original process may re-obtain 289 the atomic lock and continue executing its block atomically. 284 290 285 291 If a statement inside an atomic block blocks, so that the process executing the atomic block has no enabled statement, execution deadlocks. 286 The exception to this rule is that the first statement in the atomic block, and the first statement after a `$yield`, as described above, may block, without necessarily causing deadlock. 292 The exception to this rule is that the first statement in the atomic block, and the first statement after a `$yield`, as described above, 293 may block, without necessarily causing deadlock. 287 294 288 295 Atomic blocks may be nested. … … 291 298 Each time it leaves an atomic block, the multiplicity is decremented. 292 299 When the multiplicity hits 0, the atomic lock is released. 293 Execution of a `$yield` does not change the multiplicity; the process releases the lock but maintains the multiplicity, so that when the lock is re-obtained, the original multiplicity is still in place. 300 Execution of a `$yield` does not change the multiplicity; the process releases the lock but maintains the multiplicity, 301 so that when the lock is re-obtained, the original multiplicity is still in place. 294 302 295 303 === Nondeterministic selection statement `$choose` … … 312 320 The implicit guard of the `$choose` statement with a default clause is ''true''. 313 321 314 Example: this shows how to encode a “low-level” guarded transition system: 322 ==== Example 323 This shows how to encode a “low-level” guarded transition system: 315 324 {{{ 316 325 l1: … … 362 371 363 372 The semantics are as follows: when control reaches the loop, one process is spawned for each element of the domain. 364 That process has local variables corresponding to the iteration variables, and those local variables are initialized with the components of the tuple for the element of the domain that process is assigned. 373 That process has local variables corresponding to the iteration variables, and those local variables are initialized with the components 374 of the tuple for the element of the domain that process is assigned. 365 375 Each process executes the statement ''S'' in this context. 366 376 Finally, each of these processes is waited on at the end. … … 373 383 $when (expr) stmt; 374 384 }}} 375 All statements have a guard, either implicit or explicit. For most statements, the guard is ''true''. The `$when` statement allows one to attach an explicit guard to a statement. 385 All statements have a guard, either implicit or explicit. For most statements, the guard is ''true''. 386 The `$when` statement allows one to attach an explicit guard to a statement. 376 387 377 388 When `expr` is ''true'', the statement is enabled, otherwise it is disabled. … … 522 533 In the symbolic semantics, this function assigns a fresh symbolic constant of the appropriate type to the object pointed to by `ptr`. 523 534 524 === Hiding pointers from the reachability analyzer: `$hide`, `$reveal`, and `$hidden`535 === Hiding pointers: `$hide`, `$reveal`, and `$hidden` 525 536 526 537 The partial order reduction algorithm used by the CIVL Model Checker computes the set of memory locations that a process ''p'' can reach. … … 530 541 graph are the reachable objects of ''p''. 531 542 532 There are times when one wants to modify this directed graph by ignoring some edge. The purpose of these functions is to provide a way to do this from CIVL-C code. 543 There are times when one wants to modify this directed graph by ignoring some edge. 544 The purpose of these functions is to provide a way to do this from CIVL-C code. 533 545 The signatures are: 534 546 {{{ … … 537 549 $system _Bool $hidden(const void* ptr); 538 550 }}} 539 Function `$hide` wraps a pointer object in another object which is opaque to the reachability analyzer, i.e., the analyzer will not look inside this object and therefore will not find the hidden pointer. Nothing can be done with this hidden pointer until it is "revealed", i.e., extracted from the opaque object. The function `$hidden` tells whether its argument is a value returned by `$hide`. 540 541 === Checking whether a pointer dereference is safe: `$is_derefable` 551 Function `$hide` wraps a pointer object in another object which is opaque to the reachability analyzer, i.e., the analyzer will not look inside 552 this object and therefore will not find the hidden pointer. 553 Nothing can be done with this hidden pointer until it is "revealed", i.e., extracted from the opaque object. 554 The function `$hidden` tells whether its argument is a value returned by `$hide`. 555 556 === Checking pointer safety: `$is_derefable` 542 557 543 558 This function has signature … … 548 563 This means `ptr` points to a memory location that is capable of and is currently holding a value of type T, where T is the type of `*ptr`. 549 564 550 === `$is_terminated`565 === Checking process termination: `$is_terminated` 551 566 552 567 Signature:
