blob: 77ea3d7a7ae16340d608d8ca570a6d0ea9c9e545 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
+++
title = "Semantics of predicates in the abstract"
date = "2023-02-04"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3f"]
forwardlinks = ["3c3f2"]
zettelid = "3c3f1"
+++
In the abstract language, which is used to verify the schedules produced
by the scheduler, it also has to verify the equivalence of the
predicates. However, these predicates have rich semantics, because they
include expressions that are taken from the code during the symbolic
evaluation. This, however, means that these predicates do not always
evaluate to a value, as the context might not contain enough information
to evaluate an expression. In addition to that, it's not certain that
the expressions are free of undefined behaviour when they are evaluated
with an arbitrary context, which would mean that a division that was
safe in the input could suddenly become a division by 0.
|
