1 files changed, 36 insertions, 0 deletions
diff --git a/content/zettel/3a5c.md b/content/zettel/3a5c.md
new file mode 100644
index 0000000..7148e8d
--- /dev/null
+++ b/content/zettel/3a5c.md
@@ -0,0 +1,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.