본문 바로가기
  • Home

Deterministic Parallelism for Symbolic Execution Programs based on a Name-Freshness Monad Library

  • Journal of The Korea Society of Computer and Information
  • Abbr : JKSCI
  • 2021, 26(2), pp.1-9
  • DOI : 10.9708/jksci.2021.26.02.001
  • Publisher : The Korean Society Of Computer And Information
  • Research Area : Engineering > Computer Science
  • Received : January 7, 2021
  • Accepted : February 3, 2021
  • Published : February 26, 2021

Ki Yung Ahn 1

1한남대학교

Accredited

ABSTRACT

In this paper, we extend a generic library framework based on the state monad to exploit deterministic parallelism in a purely functional language Haskell and provide benchmarks for the extended features on a multicore machine. Although purely functional programs are known to be well-suited to exploit parallelism, unintended squential data dependencies could prohibit effective parallelism. Symbolic execution programs usually implement fresh name generation in order to prevent confusion between variables in different scope with the same name. Such implementations are often based on squential state management, working against parallelism. We provide reusable primitives to help developing parallel symbolic execution programs with unbound-genercis, a generic name-binding library for Haskell, avoiding sequential dependencies in fresh name generation. Our parallel extension does not modify the internal implementation of the unbound-generics library, having zero possibility of degrading existing serial implementations of symbolic execution based on unbound-genecrics. Therefore, our extension can be applied only to the parts of source code that need parallel speedup.

Citation status

* References for papers published after 2023 are currently being built.

This paper was written with support from the National Research Foundation of Korea.