This repository contains mechanized proof of "Verified Validation for Affine Polyhedral Scheduling" in the Coq proof assistent. It contains a general verified validation framework (PolCert), and its verified instantiation of a CompCert instruction's variant (CInstr). The algorithm's completeness is evaluated with the Pluto compiler.

@InProceedings{10.1007/978-3-031-64626-3_17,
author="Li, Xuyang
and Liang, Hongjin
and Feng, Xinyu",
editor="Chin, Wei-Ngan
and Xu, Zhiwu",
title="Verified Validation for Affine Scheduling in Polyhedral Compilation",
booktitle="Theoretical Aspects of Software Engineering",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="287--305",
abstract="Structural nested loops can be abstracted into polyhedral models, based on which one can perform aggressive loop optimizations; however, the optimizations are often heuristic and complex, and therefore error-prone. Meanwhile, verified compilers, though rigorously correct, still miss powerful optimizing transformations and therefore produce less efficient code than industrial ones. To bridge this gap, this work provides a general verified validation framework based on Bernstein's conditions for affine scheduling, the core component of polyhedral optimization techniques. It is parameterized over the concrete definitions and proofs of the instruction language to be reusable. As shown in our evaluation, the framework is flexible enough to support both existing verified compilers like CompCert and existing polyhedral compilers like Pluto. The result is fully mechanized in the Coq proof assistant.",
isbn="978-3-031-64626-3"
}

Acknowledgement: This project bases on Verified Polyhedra Library (VPL) and PolyGen, and similar idea can be found at s2sloop.

The validator takes two polyhedral models (before and after auto-transformation like pluto's core algorithm), and output their equivalence (equal or unknown). It can only deal with two polyhedron models with strictly equal instructions, differing only in schedule (scattering) functions (then only supports reordering of instances, not supporting tiling etc). The validation algorithm just constructs test polyhedrons for all WAW/WAR/RAW dependences (write/read access functions should be given) for their violation.

Users should instantiate their own Instr, which merely demands the language's semantics implies permutability under Bernstein’s Conditions; this needs users to provide a verified checker function (like, basing on symbolic execution) for validity of read and write access functions regarding to the semantics. As an example, we provide CompCert's instruction (called CInstr) as its instantiation and parameterize the validator (see CPolOpt.v). Note that, we wrap the Pluto compiler with the validator to achieve verified compilation. Nevertheless, there's still several challenges to (seamlessly) integrate polyhedral compilation into CompCert as an extension, like machanizing a verified extractor, dealing with assumptions (heavy static reasoning) of polyhedal compilation (optimistic approach seems possible, but at least need to change CompCert's semantics for overflow flag (see this report)), more complete scheduling supports, vectorization and parallemism... Also, we find PolyGen (see this issue) need extra constraints to restrict the length of iteration vector (i.e., depth), which is not convenient and is not compatible to, like, Pluto's output format; we introduce additional field depth in the polyhedral model to simplify this, but this leads to a (small) semantics gap. Some efforts are needed to reuse PolyGen's proof, though it is now compiled together with ours.

An executable polcert can be extracted and runs on two polyhedron models in OpenScop format (of course, there's conversion between OpenScop and our inner representation). Though, as Openscop format does not contain information like typing and can be complex eough, we can not give it valid semantics (like CInstr). Only the algorithms are reused. Access function's consistency to instruction's semantics is then lifted as assumption. With these in mind, the algorithm is tested on pluto's 62 test cases. See TInstr and TPolValidator for this trivial instantiation.

Main proofs can be found in ./src folder. Unit tests are in ./tests folder; ./tests/pluto-all includes all 62 test cases evaluated with Pluto.

For more complete project information, see documentation.

.
├── Dockerfile, Makefile[...], configure
├── README.md
├── doc                # Chore: for documentation 
├── src                # Coq: main machanization of this project
├── VPL                # Coq: Verified Polyhedra Library
├── polygen            # Coq: PolyGen's machanization
├── flocq              # Coq: Floating point Library, used by CompCert
├── cfrontend, common, lib, x86, x86_64  # Coq: (mainly) CompCert Coq files
├── tests              # Chore: test suit and test scripts
├── cparser, driver    # OCaml: compiler driver, amended from CompCert's
├── extraction         # Chore: for coq file's ocaml extraction 
├── samples            # Coq: sample polyhedral programs (instantiate with CInstr) 
├── tools              # Chore: just some tools
└── MenhirLib          # TBD: the verified parser, may reuse it later, now useless

We recommand you to test our implementation with docker. You can build the docker image from scatch with (see Dockerfile):

# this may take (less-than) 30 minutes, depend on your network condition
docker build . -t polcert

You can also fetch the offical image (may not be updated in time, but it should work) from the provided docker-hub repository by:

docker pull hughshine/polcert:latest

Then you can run the project inside the docker:

sudo docker run -p 80:80 -ti [--rm] [hughshine/]polcert:latest

Inside the docker container, try the following command to build the project:

make -j4  # compile coq proofs and extract an executable
make install  # install the executable to PATH, invoke with 'polcert <pol1> <pol2>'
make test # runs all unit tests & evaluation on pluto (output file `result.txt`)
# cat result.txt
## Test (just test name) ToP (time of pluto's auto-transformation, ms) ToB (time of backward refinement validation, ms) ToF (time of forward refinement validation, ms) Result (EQ/LT/GT/NE)
## covcol 4.12 366.14 294.55 EQ
## dsyr2k 2.96 103.09 79.98 EQ
## ...
# make clean && make camlclean # if your project break

You can run make check-admitted for unfinished proofs. No additional axioms are introduced (you have to manually check this). You can count lines of code of Coq with cloc with make loc (note that the satistics is not complete, but roughly accurate; we added some code to library files).

For the docker image, it bases on prebuild pluto base image (we modify pluto to dump its intermediate representation), installs coq/ocaml environment (and some tools), and prepares the configuration. See the Dockerfile for more details. If you want to install the project manually, just follow the steps in Dockerfile.

You can generate project's full documentation by make documentation (After running make) and view it at localhost (If you use the docker image).

If your build and installation succeeds, there should be executable polcert in your PATH. pluto (see here) is already in your path. Now you can write your own test case (vim is provided in the image) like test.c,

#pragma scop
// Your loop should be surrounded with pragma
// You don't need to write complete c program, as pluto intercepts the fragment
#pragma endscop

and then invoke pluto with

pluto --dumpscop --nointratileopt --nodiamond-tile --noprevector \
      --smartfuse --nounrolljam --noparallel --notile --rar test.c

If compilation succeeds, intermediate files (see OpenScop format) are generated:

ls *.scop
# test.afterscheduling.scop
# test.beforescheduling.scop

The run polcert <pol1> <pol2> on them. Note that polcert tries to run the validation algorithm twice, so any order is ok.

polcert test.beforescheduling.scop test.afterscheduling.scop

It will give output like:

[EQ] The two polyhedral models (test.beforescheduling.scop, test.afterscheduling.scop) are equivalent.
# or
[GT] Polyhedral model test.beforescheduling.scop refines test.afterscheduling.scop.
# or
[LT] Polyhedral model test.afterscheduling.scop refines test.beforescheduling.scop.
# or
[NE] Cannot determine refinement relations between the two polyhedral models (test.afterscheduling.scop, test.beforescheduling.scop).

We turn off several warnings for clarity. Three additional (and unimportant) Coq warnings were turned off comparing to CompCert. OCaml's warnings are not discussed as they do not affect formal guarantees (most of them come from extracted VPL code).

Coq compilation (see Makefile):

1. -unused-pattern-matching-variable: disabled in CompCert
2. -deprecated-ident-entry: disabled in CompCert
3. -implicit-core-hint-db: inherit from PolyGen, to be solved upsteam
4. -deprecated-hint-without-locality: inherit from PolyGen, to be solved upsteam
5. -undeclared-scope: library file, to be solved

Coq extraction (see extraction.v):

1. -extraction-ambiguous-name, does not matter
2. -extraction-opaque-accessed, to be fixed in VPL

Ocaml compilation (see Makefile.extr).

See LICENSE. We follow PolyGen.