|
1 | | -# polcert |
| 1 | +# Standalone Validation with polcert |
2 | 2 |
|
3 | | -`polcert` checks externally supplied polyhedral transformations without |
4 | | -running loop extraction or code generation. It accepts OpenScop models and |
5 | | -uses the same verified affine and tiling validators as `polopt`. |
| 3 | +`polcert` checks supplied polyhedral models without running the complete |
| 4 | +loop-to-loop compiler. It uses the affine and tiling validators also used by |
| 5 | +`polopt`. Build instructions are in [Environment](ENVIRONMENT.md). |
6 | 6 |
|
7 | | -## Affine scheduling |
| 7 | +## Affine Scheduling |
8 | 8 |
|
9 | 9 | ```sh |
10 | 10 | ./polcert before.scop after.scop |
11 | 11 | ``` |
12 | 12 |
|
13 | | -The models must describe the supported common instructions, domains, and |
14 | | -accesses. The validator checks whether the changed schedule preserves the |
15 | | -required dependences. This is not a validator for arbitrary C programs. |
| 13 | +Supply two OpenScop models with the supported common domains and accesses. |
| 14 | +The checker tests whether the new schedule preserves required dependence |
| 15 | +orders. It omits instruction bodies and relies on the supplied access |
| 16 | +summaries and memory model. Acceptance is consequently a model-level result, |
| 17 | +not a proof of arbitrary C-program equivalence. |
16 | 18 |
|
17 | | -## Tiling and subsequent scheduling |
| 19 | +## Tiling and Phase Composition |
18 | 20 |
|
19 | 21 | ```sh |
20 | 22 | ./polcert --kind tiling mid.scop posttile.scop |
21 | 23 | ./polcert before.scop mid.scop posttile.scop |
22 | 24 | ./polcert before.scop mid.scop posttile.scop after.scop |
23 | | -./polcert --second-level-tile --kind tiling mid.scop posttile.scop |
24 | 25 | ``` |
25 | 26 |
|
26 | 27 | The three-file form checks affine scheduling followed by tiling. The four-file |
27 | | -form also checks the final affine transformation, as used by diamond tiling |
28 | | -and intra-tile scheduling. Intermediate files describe actual stage results; |
29 | | -their names alone do not establish that they form a valid pipeline. |
| 28 | +form adds post-tiling affine validation. Add `--second-level-tile` for the |
| 29 | +corresponding two-level layout. These files must represent actual consecutive |
| 30 | +stage results; [Pluto interface](doc/PLUTO_INTERFACE.md) explains the exports. |
30 | 31 |
|
31 | | -A successful tiling check reports `permutable-band`. Unsupported layouts and |
32 | | -failed band conditions are rejected; solver alarms propagate as failures. |
33 | | -The tiling dispatcher does not fall back to general affine validation. |
| 32 | +A runnable positive control is: |
34 | 33 |
|
35 | | -The [Pluto interface](doc/PLUTO_INTERFACE.md) describes how to obtain the |
36 | | -corresponding `.beforescheduling.scop`, `.midtransform.scop`, |
37 | | -`.posttile.scop`, and `.afterscheduling.scop` files. |
| 34 | +```sh |
| 35 | +./polcert --kind tiling \ |
| 36 | + tools/tiling_routes/fixtures/diamond-tile-example.midtransform.scop \ |
| 37 | + tools/tiling_routes/fixtures/diamond-tile-example.posttile.scop |
| 38 | +``` |
| 39 | + |
| 40 | +Expect acceptance through `permutable-band`. Failed recognition, failed band |
| 41 | +conditions, or solver alarms do not certify a proposal. Tiling has no fallback |
| 42 | +to general affine validation. |
38 | 43 |
|
39 | | -## Index-set splitting |
| 44 | +## Index-Set Splitting |
40 | 45 |
|
41 | 46 | ```sh |
42 | 47 | ./polcert --iss-bridge bridge.txt |
43 | 48 | ./polcert --iss-debug-dumps before.txt after.txt |
44 | 49 | ``` |
45 | 50 |
|
46 | | -These modes check the imported ISS structure. For an end-to-end ISS |
47 | | -compilation with semantic refinement, use `polopt --iss`; a standalone bridge |
48 | | -check is not itself a loop-to-loop compilation theorem. |
| 51 | +These modes check imported partition structure. The |
| 52 | +[ISS fixtures](tests/iss-pluto-dumps/README.md) describe the input formats and |
| 53 | +positive/negative expectations. Use `polopt --iss` when the desired result is |
| 54 | +a compiled loop with an end-to-end refinement theorem. |
49 | 55 |
|
50 | | -## Results and scope |
| 56 | +## Interpreting Results |
51 | 57 |
|
52 | | -Inspect the exit status as well as the validation message. A command may |
53 | | -reject a proposal or fail to construct a supported checking problem; neither |
54 | | -outcome certifies that proposal. Regression tests require the expected stage |
55 | | -and acceptance or rejection, not merely the presence of an output file. |
| 58 | +Check both the exit status and diagnostic. Rejection can mean an illegal |
| 59 | +proposal, a conservative dependence check, or unsupported input structure. |
| 60 | +A solver alarm is a failure to certify, not evidence that the transformation |
| 61 | +is safe. Successful standalone checks do not perform extraction or code |
| 62 | +generation and cannot establish their guarantees. |
56 | 63 |
|
57 | | -Parsing and OpenScop import are engineering interfaces around the extracted |
58 | | -validators. The formalization is parameterized by the instruction semantics; |
59 | | -the executable instantiation and its limitations are described in |
60 | | -[Verified pipeline](doc/VERIFIED_PIPELINE.md). |
| 64 | +For compiler-stage contracts and the concrete instruction model, read |
| 65 | +[Verified Pipeline](doc/VERIFIED_PIPELINE.md). |
0 commit comments