OGST - Jieung Kim
Title : Compositional Semantics for Concurrent Object with Scheduling
Abstract: Trace-based program analysis is a prominent way to analyze the meaning of the program without knowing the detailed implementation of it. In most cases of trace-based program analysis, programs generate events during their evaluations, and traces are usually defined as a sequence of events achieved by program executions. Using this approach, traces may contain the most important information of the program execution, and therefore people can utilize the trace to analyze the desired property of the program. Apparently, trace-based semantics are also used to analyze concurrent programs, which is quite common these days. Currently, when trace-based semantics come with concurrency, some are dealing with program state sharing and others are dealing with linearizability of the concurrent program, which is well known for its correctness condition for parallel programs. Concurrent program, however, basically has non-deterministic characteristic, but a few of them are considering analyzing concurrent programs in deterministic ways. This implies that those works are hard to combine with CompCert, one of the most eminent tools in the program verification area. This is because of the fact that the current CompCert only supports the sequential execution. This current limitation on both works let us know that finding a way to extract the deterministic execution paths in a concurrent program evaluation is necessary. Therefore, we focus on finding out the way to achieve deterministic program path of concurrent object as compositional way. Specifically, we design a language with concurrency and explicit scheduling commands, so that the language supports fine-grained compositional program analysis. By doing that, we believe we can establish a basic stone for connecting CompCert and concurrent program analysis.