Changes between Version 28 and Version 29 of ContractReduction


Ignore:
Timestamp:
12/07/15 13:28:57 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v28 v29  
    22
    33== ACSL function contract grammar with CIVL-C extension (starting with `$`) ==
     4The CIVL-C function contract extends ACSL function contract with the following elements:
     5* `$guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body
     6* `$depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
     7* `$reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
     8
    49{{{
    510function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause?
    … …  
    7479where `event` is a memory event represented as a boolean expression.   For each process `p`, the `event ` can be evaluated in the context of `p`.   If `event ` evaluates to `true`, then `p` must be included in an ample set containing a call to this function.
    7580
     81The grammar of `event` is defined as follows:
     82
     83{{{
     84EventSetExpression
     85 ::= $read(MemorySetExpression)
     86 | $write(MemorySetExpression)
     87 | $access(MemorySetExpression)
     88 | $calls(FunctionCallExpression)
     89 | \nothing
     90 | $everything
     91 | ‘(’ EventSetExpression ‘)’
     92 | EventSetExpression + EventSetExpression
     93 | EventSetExpression - EventSetExpression
     94 | EventSetExpression & EventSetExpression
     95}}}
     96
    7697The expression `event ` hence defines a predicate d(s,p), where s ranges over states, and p over procs.   The requirement is the following:
    7798
    … …  
    163184
    164185
    165 == Function specifiers ==
    166 
    167 Both `$atomic` and `$atom` may be used as function specifiers.   They designate that any call to the function is to be treated atomically or atom-ly, respectively.
     186== Function specifier `$atomic_f`==
     187The function specifier `$atomic_f` may be used to designate that any call to the function is to be treated atomically.
    168188
    169189== Guards ==
    170190
    171 The following construct is used to specify a guard for a function.  The function may be a system or ordinary function.  It maybe used in conjunction with `$atom` or `$atomic`.
     191The following construct is used to specify a guard for a function.  The function may be a system or ordinary function.  It maybe used in conjunction with `$atomic_f`.
    172192Grammatically, it is a contract clause, though it is not really part of the contract. 
    173193
    … …  
    182202- The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set.
    183203{{{
    184 void comm_dequeue($comm comm, ....)
    185   $depends {$access(*comm)}
    186 ;
    187 }}}
     204/*@ $depends $access(*comm); */
     205void comm_dequeue($comm comm, ....);
     206}}}