A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model

Abstract:

Concurrent randomized programs under the oblivious adversary model are extremely difficult for modular verification because the interaction between threads is very sensitive to the program structure and the execution steps. We propose a new program logic supporting thread-local verification. With a novel "split" mechanism, one can split the state distribution into smaller partitions, and the reasoning can be done based on each partition independently, which allows us to avoid considering different execution paths of if-statements and while-loops simultaneously. The logic rules are compositional and are natural extensions of their sequential counterparts. Using our program logic, we verify four typical algorithms under the oblivious adversary model.

Authors:

Weijie Fan
Hongjin Liang
Xinyu Feng
Hanru Jiang

To appear:

In Proc. 34th European Symposium on Programming (ESOP'25).