Content area
Many properties of programs can be expressed through quantities such as power consumption, memory usage, execution time, the number of function calls, etc. Controlling these quantities can improve program reliability, security, privacy, usability, etc. For instance, the performance in terms of the execution time of two pieces of code for the same task can be used to decide which one to use. Providing tight bounds on these quantities is useful to improve software design for different potential applications. In this dissertation, I will focus on several different quantitative properties of programs that can be used to improve programs’ performance, along different axes.
The first domain is relational cost analysis, which aims to provide tight bounds on the difference of the costs of evaluating two programs. The cost here is abstract, can be execution time, reduction step or number of functions calls, etc. Relational cost analysis earned people's attention for its application in program optimization and side-channel attack detection. Most of the related works have focused on pure functional programs. However, these reasoning principles may not be directly applied to situations where the program uses some effect, for example, destructive updates. To increase the expressiveness, we propose a type and effect system ARel to enable precise relational cost analysis over high-order functional programs, with mutable arrays, an important imperative feature. It can be regarded as the first step toward relational cost analysis for functional imperative programs with mutable state. Additionally, relational type and effect systems such as ARel suffer from the lack of methodology of implementation. To fill this gap, we propose a bidirectional type checking methodology to algorithmize these systems.
Another quantity is the adaptivity in adaptive data analysis, where the queries asked by data analysts may depend on the results of previous queries. If we represent the interactions with a data analyst as a program, we can find some chain of queries so that every query may rely on the previous query in the chain. The adaptivity of this program is defined to be the length of the longest chain of queries. Reasoning about adaptivity helps to choose the appropriate statistical technique to use to control the generalization error of the data analysis. We propose a program analysis algorithm to statically estimate adaptivity.
