Towards Performance Evaluation Programming

摘要

In recent work we have introduced an experimental concurrent programming language which supports a systematic approach to performance analysis and formal verification correlated with a programming style called performance evaluation programming [19]. For the purpose of formal verification, the ranges of variables must be bounded and concurrent programs are translated into corresponding (finite state) Continuous Time Markov Chains (CTMCs) which are analyzed by using the PRISM tool. Activities in a CTMC model are abstracted by their rates. In the language introduced in [19] an activity is the evaluation of a function expressed in a functional sub-language. The solution presented in [19] supports formal verification in a systematic manner, but not automatically, requiring the programmer to generate certain data for the performance evaluation experiments. In this paper we refine the design of the functional sub-language introduced in [19] by using concepts of functional programming with dependent types. We use dependent types to control the ranges of variables. The solution presented in this paper is devised to support automatic performance evaluation and formal verification of (bounded versions of) concurrent programs.