1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
+++
title = "Mutliple to one step simulation"
date = "2022-04-24"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5c"]
forwardlinks = ["3c3h1", "1b6", "3c3", "3a5c1a"]
zettelid = "3a5c1"
+++
This has been implemented in CompCert-KVX ([\#3c3h1]) \[1\] (Figure 12).
The main problem that is often encountered is that you want to do
multiple steps in the source language, and only one step in the output
language. One example of this is when adding basic blocks ([\#1b6]) to
the target language. In this case, one will often define the execution
of the basic block using big-step semantics, as otherwise there would
not be a great benefit of using these semantics. These semantics are
useful for proving scheduling ([\#3c3]), for example. However, this
means that the semantics are not in a one to one correspondence anymore.
The traditional way to prove a forward simulation between a source and a
target language is by using a simulation in lock-step, where one step in
the input corresponds to one step in the output. However, a
generalisation of this is to allow for the fact that one step in the
input could match one or more steps in the output semantics. This is
directly supported by the small step semantics framework inside of
CompCert. Finally, another generalisation is that one step in the input
could correspond to zero or more steps in the output. This comes with
the limitation that one has to show that the semantics will not get
stuck, meaning there is some constantly decreasing metric when one is
not performing a step.
However, none of these things directly solve the issue of having to
perform multiple step in the input to be able to even do one step in the
output. To do this, one will have to abuse the star simulation (zero or
more steps), but keep track of the previous steps that one has already
performed to be able to reconstruct the proof from the start of the
output step to the end of the output step. This can be done by always
performing a `star_refl` step (don't perform a step), but still create a
way to match states until one reaches the end of the output step.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-six22_formal_verif_super_sched" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">C. Six, L. Gourdin, S. Boulmé, D.
Monniaux, J. Fasse, and N. Nardino, “Formally verified superblock
scheduling,” in *Proceedings of the 11th ACM SIGPLAN international
conference on certified programs and proofs*, in CPP 2022. Philadelphia,
PA, USA: Association for Computing Machinery, 2022, pp. 40–54. doi:
[10.1145/3497775.3503679].</span>
</div>
</div>
[\#3c3h1]: /zettel/3c3h1
[\#1b6]: /zettel/1b6
[\#3c3]: /zettel/3c3
[10.1145/3497775.3503679]: https://doi.org/10.1145/3497775.3503679
|
