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
|
+++
title = "Forward Simulation"
date = "2020-12-10"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a5b"]
forwardlinks = ["3a5d", "3a5c1"]
zettelid = "3a5c"
+++
Forward simulation is a bit less informative, because it only says that
if the source has some behaviour *B*, then the output will have the same
behaviour. However, it might be that the output has some other behaviour
in addition to that, which would still satisfy the property of forward
simulation. These behaviours would be unwanted behaviours of *C* which
are on top of the behaviours that *S* has.
$\forall B,\ S \Downarrow B \implies C \Downarrow B$
This is not possible when *C* is deterministic though, meaning that
there is only one observable behaviour of *C*
($C \Downarrow B_1 \land C \Downarrow B_2\implies B_1 = B_2$). If that
is the case, then the forward simulation also implies the backwards
simulation, as there is no other behaviour that *C* could have.
As forward simulation is simpler to prove, it is used instead of a
backward simulation together with a proof that the target language is
deterministic. The latter proof of determinism is especially simple in
CompCert, because the intermediate languages are single-threaded
assembly languages that are inherently deterministic. In the case of
compilation to hardware, this might be more difficult, because hardware
is inherently parallel and nondeterministic. It would therefore have to
conform to the specification no matter what path was taken. It might
therefore also not be possible to follow the same proof, and one would
have to prove the backward simulation directly.
|
