Publications

@inproceedings{10.1007/978-3-030-99527-0_18,
title = {Alpinist: An Annotation-Aware GPU Program Optimizer},
author = {Ömer {Ş}akar and Mohsen Safari and Marieke Huisman and Anton Wijs},
editor = {Dana Fisman and Grigore Rosu},
url = {https://doi.org/10.1007/978-3-030-99527-0_18},
doi = {10.1007/978-3-030-99527-0_18},
isbn = {978-3-030-99527-0},
year = {2022},
date = {2022-01-01},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
pages = {332--352},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@inproceedings{10.1007/978-3-030-90636-8_7,
title = {A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions},
author = {Jan Martens and Jan Friso Groote and Lars van den Haak and Pieter Hijma and Anton Wijs},
editor = {Gwen Salaün and Anton Wijs},
url = {https://doi.org/10.1007/978-3-030-90636-8_7},
doi = {10.1007/978-3-030-90636-8_7},
isbn = {978-3-030-90636-8},
year = {2021},
date = {2021-01-01},
booktitle = {Formal Aspects of Component Software},
pages = {115--133},
publisher = {Springer International Publishing},
address = {Cham},
abstract = {The most efficient way to calculate strong bisimilarity is by finding the relational coarsest partition of a transition system. We provide the first linear-time algorithm to calculate strong bisimulation using parallel random access machines (PRAMs). More precisely, with n states, m transitions and $$| Act |backslashle m$$|Act|≤maction labels, we provide an algorithm for $$backslashmax (n,m)$$max(n,m)processors that calculates strong bisimulation in time $$backslashmathcal O(n+| Act |)$$O(n+|Act|)and space $$backslashmathcal O(n+m)$$O(n+m). The best-known PRAM algorithm has time complexity $$backslashmathcal O(nbackslashlog n)$$O(nlogn)on a smaller number of processors making it less suitable for massive parallel devices such as GPUs. An implementation on a GPU shows that the linear time-bound is achievable on contemporary hardware.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@inproceedings{vandenHaak2020,
title = {Formal methods for GPGPU programming: is the demand met?},
author = {Lars B. van den Haak and Anton Wijs and Mark van den Brand and Marieke Huisman},
url = {https://doi.org/10.1007/978-3-030-63461-2_9},
doi = {10.1007/978-3-030-63461-2_9},
year = {2020},
date = {2020-11-26},
booktitle = {Integrated Formal Methods},
publisher = {Springer International Publishing},
series = {Springer’s Lecture Notes in Computer Science},
abstract = {Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed sofar are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}

@inproceedings{10.1145/3427761.3428344,
title = {Towards Verified Construction of Correct and Optimised GPU Software},
author = {Marieke Huisman and Anton Wijs},
url = {https://doi.org/10.1145/3427761.3428344},
doi = {10.1145/3427761.3428344},
isbn = {9781450381864},
year = {2020},
date = {2020-01-01},
booktitle = {Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs},
pages = {10–14},
publisher = {Association for Computing Machinery},
address = {Virtual, USA},
series = {FTfJP 2020},
abstract = {Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}