1. Rewrite your method zeroAll (exercise series 1) as parallel block
and verify your new implementation (both data race freedom and
functional correctness). 

2. Write a PVL encoding of the following kernel:

__kernel bla (__global float* a) {
	int tid = get_global_id(0);
        int tmp = a[tid];
	if (tid > 0) {
          tmp = a[tid] + a[tid – 1];
    }
	BARRIER(CLK_GLOBAL_MEM_FENCE);
	a[tid]  = tmp;  
}

Note to encode the thread local variables tmp, use an array tmp, such
that tmp[tid] is the local variable of thread tid.

Verify its permissions, and verify its functional correctness (hint:
you will have to use a ghost variable for this. In the next lecture,
this will be discussed, so don't worry if you can't solve this
completely now.)

3. Consider the class ArraySum in the file sum_reduction.pvl. This
encodes a kernel where the shared variable sum is updated by all the
thead using an atomic instruction.

a. Prove that this method does not have data races
b. Next we would like to show functional correctness. A common way to
do this is to add an extra (ghost) array contrib, which is used to
keep track for each thread how much it has contributed to the shared
variable sum. The value of the variable sum can then be expressed in
terms of the elements of this contribu array. Try to develop this
solution.

Unfortunately, due to a bug in Vercors, this is not provable yet (my
solution gives the error message: Local name globals is undefined).

c. However, if we use sequences rather than arrays, the solution is
provable. As sequences are not updateable in-place, we need to define
some functions over sequences (fresh and update), plus some lemmas (provable
properties) which relate the value of sum to the elements in the
sequence.

File sequence.pvl contains these definitions and lemmas. Now adapt
your solution to b, i.e. use a sequence of contributions, use the
functions to define the contents of contrib, and insert the lemmas in
the code wherever we need to establish the property between contrib
and sum.

4. [Optional]
Make exercise b of Challenge 3 of the VerifyThis Program Verification
Competition 2019.