Commit e5c727d8 by Ralf Jung

### apply feedback

parent 38dbbf59
 ... @@ -9,10 +9,11 @@ language for simple examples. ... @@ -9,10 +9,11 @@ language for simple examples. HeapLang is a lambda-calculus with operations to allocate individual locations, HeapLang is a lambda-calculus with operations to allocate individual locations, `load`, `store`, `CAS` (compare-and-swap) and `FAA` (fetch-and-add). Moreover, `load`, `store`, `CAS` (compare-and-swap) and `FAA` (fetch-and-add). Moreover, it has a `fork` construct to spawn new threads. In terms of values, we have it has a `fork` construct to spawn new threads. In terms of values, we have integers, booleans, unit, heap locations as well as (binary) sums and products. integers, booleans, unit, heap locations, as well as (binary) sums and products. Functions are the only binders, so the sum elimination (`Case`) expects both Recursive functions are the only binders, so the sum elimination (`Case`) branches to be of function type and passes them the data component of the sum. expects both branches to be of function type and passes them the data component of the sum. For technical reasons, the only terms that are considered values are those that For technical reasons, the only terms that are considered values are those that begin with the `Val` expression former. This means that, for example, `Pair begin with the `Val` expression former. This means that, for example, `Pair ... @@ -20,8 +21,8 @@ begin with the `Val` expression former. This means that, for example, `Pair ... @@ -20,8 +21,8 @@ begin with the `Val` expression former. This means that, for example, `Pair This leads to some administrative redexes, and to a distinction between "value This leads to some administrative redexes, and to a distinction between "value pairs", "value sums", "value closures" and their "expression" counterparts. pairs", "value sums", "value closures" and their "expression" counterparts. However, this also makes values very syntactically uniform, which we exploit in However, this also makes values syntactically uniform, which we exploit in the the definition of substitution which just skips over `Val` terms, because values definition of substitution which just skips over `Val` terms, because values should be closed and hence not affected by substitution. As a consequence, we should be closed and hence not affected by substitution. As a consequence, we can entirely avoid even talking about "closed terms", that notion just does not can entirely avoid even talking about "closed terms", that notion just does not have to come up anywhere. We also exploit this when writing specifications, have to come up anywhere. We also exploit this when writing specifications, ... @@ -47,7 +48,7 @@ eagerly. ... @@ -47,7 +48,7 @@ eagerly. ## Tactics ## Tactics HeapLang coms with a bunch of tactics that facilitate stepping through HeaLang HeapLang comes with a bunch of tactics that facilitate stepping through HeapLang programs as part of proving a weakest precondition. All of these tactics assume programs as part of proving a weakest precondition. All of these tactics assume that the current goal is of the shape `WP e @ E {{ Q }}`. that the current goal is of the shape `WP e @ E {{ Q }}`. ... @@ -72,22 +73,22 @@ Tactics to take one or more pure program steps: ... @@ -72,22 +73,22 @@ Tactics to take one or more pure program steps: Tactics for the heap: Tactics for the heap: - `wp_alloc l as "H"`: Reduce an allocation instruction and call the new - `wp_alloc l as "H"`: Reduce an allocation instruction and call the new location `l` (in the Coq context) and the assertion that we own it `H` (in the location `l` (in the Coq context) and the points-to assertion `H` (in the spatial context). You can leave away the `as "H"` to introduce it as an spatial context). You can leave away the `as "H"` to introduce it as an anonymous assertion, i.e., that is equivalent to `as "?"`. anonymous assertion, i.e., that is equivalent to `as "?"`. - `wp_load`: Reduce a load operation. This automatically finds the necessary - `wp_load`: Reduce a load operation. This automatically finds the points-to ownership in the spatial context, and fails if it cannot be found. assertion in the spatial context, and fails if it cannot be found. - `wp_store`: Reduce a store operation. This automatically finds the necessary - `wp_store`: Reduce a store operation. This automatically finds the points-to ownership in the spatial context, and fails if it cannot be found. assertion in the spatial context, and fails if it cannot be found. - `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This - `wp_cas_suc`, `wp_cas_fail`: Reduce a succeeding/failing CAS. This automatically finds the necessary ownership. It also automatically tries to automatically finds the points-to assertion. It also automatically tries to solve the (in)equality to show that the CAS succeeds/fails, and opens a new solve the (in)equality to show that the CAS succeeds/fails, and opens a new goal if it cannot prove this goal. goal if it cannot prove this goal. - `wp_cas as H1 | H2`: Reduce a CAS, performing a case distinction over whether - `wp_cas as H1 | H2`: Reduce a CAS, performing a case distinction over whether it succeeds or fails. This automatically finds the necessary ownership. The it succeeds or fails. This automatically finds the points-to assertion. The proof of equality in the first new subgoal will be called `H1`, and the proof proof of equality in the first new subgoal will be called `H1`, and the proof of the inequality in the second new subgoal will be called `H2`. of the inequality in the second new subgoal will be called `H2`. - `wp_faa`: Reduce a FAA. This automatically finds the necessary ownership. - `wp_faa`: Reduce a FAA. This automatically finds the points-to assertion. Further tactics: Further tactics: ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!