Maurice Laveaux: Verification in mCRL2 using multi-threaded algorithms: The term library.


Event Details


Currently the mCRL2 toolset uses sequential algorithms exclusively. From these sequential algorithms the term rewriting algorithm often has the most prominent run-time cost. Developing a parallel term rewriting algorithm requires an efficient term library. This library facilitates the creation and destruction of terms. In this presentation I will present several challenges that I encountered while trying to develop an efficient term library. Followed by several observations that lead to an envisioned design for a parallel term rewriting algorithm.