A kernel program (written in PVL) with forward dependencies. Barrier synchronisation is used to redistribute permissions for this. This program currently does not verify due to refactoring of the Chalice back-end (we will use Silicon from now).
Arrays, Barriers, GPU Kernels
Path to example file
Lines of code
36 lines (comments not included)
Lines of specification
16 lines (44.44% of the total)
Note, verification may take a while and has a time-out of 20 seconds.