Seyed Armin Vakil Ghahani

arXiv2026

Synthesizing Proofs Using Proof Sharding and Exploration

Distributed systems are hard to implement correctly, and subtle bugs can go undetected using traditional testing. Formal verification offers an alternative for proving the correctness of complex distributed systems. Despite previous efforts to automate and facilitate formal verification, it is still hard to integrate formal verification in software development. Programmers need to query the theorem prover repeatedly to find the correct proof of their system. This cycle of going back and forth with the theorem prover involves a lot of human intervention and is a barrier to adopting formal verification in software development. In this paper, we address the challenges of scaling formal verification in practice by reducing the human intervention required to find the correctness proof of a distributed system. We propose ProofSaX, an automated tool that shards large verification tasks and explores the proof search space for each shard independently to synthesize correctness proofs. We use controlled exploration when adding possible proof annotations to handle the search-space explosion problem. We evaluate ProofSaX on a variety of safety proofs for distributed systems. We show that ProofSaX can find the last proof annotation in 86 out of 103 proof-completion tasks, with runtimes ranging from one minute to two hours.

cs.PL↗

arXiv2018

Making Belady-Inspired Replacement Policies More Effective Using Expected Hit Count

Memory-intensive workloads operate on massive amounts of data that cannot be captured by last-level caches (LLCs) of modern processors. Consequently, processors encounter frequent off-chip misses, and hence, lose a significant performance potential. One way to reduce the number of off-chip misses is through using a well-behaved replacement policy in the LLC. Existing processors employ a variation of least recently used (LRU) policy to determine a victim for replacement. Unfortunately, there is a large gap between what LRU offers and that of Belady's MIN, which is the optimal replacement policy. Belady's MIN requires selecting a victim with the longest reuse distance, and hence, is unfeasible due to the need to know the future. Consequently, Belady-inspired replacement polices use Belady's MIN to derive an indicator to help them choose a victim for replacement. In this work, we show that the indicator that is used in the state-of-the-art Belady-inspired replacement policy is not decisive in picking a victim in a considerable number of cases, and hence, the policy has to rely on a standard metric (e.g., recency or frequency) to pick a victim, which is inefficient. We observe that there exist strong correlations among the hit counts of cache blocks in the same region of memory when Belady's MIN is the replacement policy. Taking advantage of this observation, we propose an expected-hit-count indicator for the memory regions and use it to improve the victim selection mechanism of Belady-inspired replacement policies when the main indicator is not decisive. Our proposal offers a 5.2\% performance improvement over the baseline LRU and outperforms Hawkeye, which is the state-of-the-art replacement policy.

cs.AR↗