Prev Chapter 4: Programming concepts Up Main page Chapter 6: Generic programming Next

5 The logic system

As many other programming languages, Quasar has an assert function. The assert function will evaluate the specified condition and will result in an error message when the condition is false. The assert function can be called with either one or two arguments:

assert(condition)
assert(condition, "condition is false")

In the second case, the error message is specified, which makes it easier for the user to resolve the issue. The assert function also gives hints to the compiler system (see Section 5.3↓). When the compiler is able to figure out that the condition will never be true, a compiler error will be generated! Note that this is in contrast to most existing programming languages, for which assert is simply a run-time function. The algorithm for evaluating assertions is then as follows:

The compiler checks the condition of the assertion.
There are three possible outcomes: valid, satisfiable or unsatisfiable:\begin_inset Separator latexpar\end_inset
1. If the result is unsatisfiable, a compile-time error will be generated.
2. If the result is satisfiable, the compiler will take the condition as a hint.
3. If the result is valid, the compiler is certain that the condition will be met in all situations. Therefore, the compiler may remove the assertion instruction from the program.
The compiler is either able to recognize the condition (see Section 5.3↓) or not able to do so. In the former case, a logic evaluation will be performed. In the latter case, the result is always satisfiable.
In case the result is satisfiable, the condition will still be checked at run-time.

The compiler is free to decide which assertions to take into account and also how to propagate information through the various compilation phases. The exact behavior may be controlled using compiler settings. For example, the following program may result in a compile-time error:

function [] = __kernel__ kernel (b : scalar, pos : ivec3)
assert(b==3)
endfunction
parallel_do(size(im), 2, kernel)

Here, the constant parameter value for b, is passed through the parallel_do function to the kernel function kernel. Through automatic specialization techniques (see Section 6.6↓), the Quasar compiler will know in this case that the value for b is 2, resulting in a compiler error. In the future, this behavior may be extended to even more complex scenarios.

5.1 Kernel function assertions

It is possible to call the assert function from a kernel or device function:

function [] = __kernel__ kernel (pos : ivec3)
b = 2
assert(b==3)
endfunction

Obviously, the above assertion fails. Quasar breaks with the following error message:

(parallel_do) test_kernel - assertion failed: line 23Recall that the kernel function is typically called by many threads in parallel. Therefore, the following rules apply:

When the user program catches an assertion failure from a kernel function, there is at least one thread (or position pos) for which the condition failed.
It is currently not possible to retrieve the position that corresponds to assertion failure. [J] [J] Note that the kernel function debugger in Quasar Redshift can bring a solution here.
The output of the kernel function is undetermined. Some threads may have completely finished, others may not have started. The order in which this happens is completely unspecified. In other words, when an assertion fails, the output of the kernel function should be ignored.

Kernel function assertions provide a very useful mechanism for directly debugging and verifying code on a CPU or GPU. The assertion system is also used internally by Quasar to perform vector and matrix boundary checking.

5.2 Built-in compiler functions

There are three meta functions that help with assertions. These functions are evaluated at compile-time (as indicated by the $-prefix)

‘$check(proposition)’ checks whether the specified proposition can be satisfied, given the previous set of assertions, resulting in three possible values: "Valid", "Satisfiable" or "Unsatisfiable".
‘$assump(variable)’ lists all assertions that are currently known about a variable, including the implicit type predicates that are obtained through type inference. Note that the result of ‘$assump‘ is an expression, so for visualization it may be necessary to convert it to a textual representation using ‘$str(.)‘ (to avoid the expression from being evaluated).
‘$simplify(expr)‘ simplifies logic expressions based on the knowledge that is inserted through assertions.

Usually, you will not need to call these functions directly from your code. Nevertheless, they can be useful for testing (for example in interactive mode).

5.3 Assertion types recognized by the compiler

There are different types of assertions recognized by the Quasar compiler. These assertions can be combined in a transparent way using the Boolean operators ! (inversion), && (and) and || (or).

5.3.1 Equalities

The most simple cases of assertions are the equality assertions a==b. For example:

symbolic a, b
assert(a==4 && b==6)
assert($check(a==5)=="Unsatisfiable")
assert($check(a==4)=="Valid")
assert($check(a!=4)=="Unsatisfiable")
assert($check(b==6)=="Valid")
assert($check(b==3)=="Unsatisfiable")
assert($check(b!=6)=="Unsatisfiable")
assert($check(a==4 && b==6)=="Valid")
assert($check(a==4 && b==5)=="Unsatisfiable")
assert($check(a==4 && b!=6)=="Unsatisfiable")
assert($check(a==4 || b==6)=="Valid")
assert($check(a==4 || b==7)=="Valid")
assert($check(a==3 || b==6)=="Valid")
assert($check(a==3 || b==5)=="Unsatisfiable")
assert($check(a!=4 || b==6)=="Valid")
print $str($assump(a)),",",$str($assump(b)) % prints (a==4),(b==6)

Here, we use symbolic to declare symbolic variables (variables that are not to be "evaluated", i.e. translated into their actual value since they don’t have a specific value). Next, the function assert tests whether the $check(.) function works correctly (=self-checking).

5.3.2 Inequalities

The propositional logic system can also work with inequalities:

symbolic a
assert(a>2 && a<4)
assert($check(a>1)=="Valid")
assert($check(a>3)=="Satisfiable")
assert($check(a<3)=="Satisfiable")
assert($check(a<2)=="Unsatisfiable")
assert($check(a>4)=="Unsatisfiable")
assert($check(a<=2)=="Unsatisfiable")
assert($check(a>=2)=="Valid")
assert($check(a<=3)=="Satisfiable")
assert($check(!(a>3))=="Satisfiable")

The idea is here that the inequality assertions can help the simplification of if conditions. For example,

assert(x > 10)
if x > 0
y = x
else
y = -x
endif

In this case, the if-test can be completely eliminated thereby ignoring the else-block, because it is certain that x is positive.

5.3.3 Type assertions

Type assertions are useful for 1) checking whether a variable has a given type and 2) for giving hints to the compiler. For example, as mentioned in Section 2.2↑, we may use a type assertion to make sure that data read from a file has the right type:

[A, B] = load("myfile.dat")
assert(type(A,"ccube") && type(B,"vec"))

Please note that assertions should not be used with the intention of variable type declaration. To declare the type of certain variables type annotations can be used:

[A : ccube, B : vec] = load("myfile.dat")Type annotations should be used on the first occurrence of a variable. In this case, the type annotation prevents A and B from becoming a polymorphic variable (see Section 4.1↑). For type assertions, there is no such requirement (they can be used in combination with a polymorphic variable).

5.4 User-defined properties

It is also possible to define "properties" of variables, using a symbolic declaration. For example:

symbolic is_a_hero, Jan_AeltermanThen you can assert:

assert(is_a_hero(Jan_Aelterman))Correspondingly, if you perform the test:

print $check(is_a_hero(Jan_Aelterman)) % Prints: Valid
print $check(!is_a_hero(Jan_Aelterman)) % Prints: Unsatisfiable

If you then try to assert the opposite:

assert(!is_a_hero(Jan_Aelterman))The compiler will complain:

assert.q - Line 119: NO NO NO I don’t believe this, can’t be true!
Assertion ’!(is_a_hero(Jan_Aelterman))’ is contradictory with ’is_a_hero(Jan_Aelterman)’

5.5 Unassert

In some cases, it is neccesary to undo certain assertions that were previously made. For this task, the function ‘unassert‘ can be used:

unassert(propositions)This function only has a meaning at compile-time; at run-time nothing needs to be done. For example, if you wish to reconsider the assertion ‘is_a_hero(Jan_Aelterman)‘ you can write:

unassert(is_a_hero(Jan_Aelterman))
print $check(is_a_hero(Jan_Aelterman)) % Prints: Satisfiable
print $check(!is_a_hero(Jan_Aelterman)) % Prints: Satisfiable

Alternatively you could have written:

unassert(!is_a_hero(Jan_Aelterman))
print $check(is_a_hero(Jan_Aelterman)) % Prints: Valid
print $check(!is_a_hero(Jan_Aelterman)) % Prints: Unsatisfiable

5.6 The role of assertions

In Quasar, the role of assertions is two-fold:

It helps to early detect logical errors (mistakes by the programmer)
It serves as a technique used for optimization. Firstly, assertions can specified upper bounds for variables, which help the compiler / code generator for the specific back-ends to generate more efficient code. Secondly, assertions can help eliminating branches in the code that are never used, as in the following example:
assert(x > 0)
if x > 20
y = x - 20
elseif x < -20
y = x + 20
else
y = 0
endif
In this case, the branch x < -20 can be completely eliminated, because it is known that x > 20.

Prev Chapter 4: Programming concepts Up Main page Chapter 6: Generic programming Next