一句话：在 Iris/Zoo 中实现并验证 OCaml 5 并行调度器，验证 Chase-Lev 工作窃取队列，提出 Iris 预言变量新抽象。
OCaml 5 引入并行域，其并行调度器（如 Domainslib）依赖工作窃取进行负载均衡，但其并发正确性缺乏机器验证。本文在基于 Iris 的 Zoo 框架中实现并机器验证了一个实际的 OCaml 5 并行调度器；该调度器具有灵活接口，既支持工作窃取，也支持其他调度策略。作为验证的一部分，作者验证了 Saturn 库中的 Chase-Lev 工作窃取双端队列，发现其具有微妙的、依赖外部与未来的线性化点，并为此在 Iris 中引入用于推理预言变量的新抽象。基准测试表明，该调度器性能与 OCaml 生态中其他调度器相当。
We present the implementation and mechanized verification of a realistic parallel scheduler for OCaml 5 using the Iris-based Zoo framework. Similarly to Domainslib, it relies on a work-stealing strategy to perform load balancing but also supports other scheduling strategies thanks to its flexible interface. e provide basic benchmarks demonstrating that its performance is on par with other schedulers from the OCaml ecosystem. As part of this effort, we verify the Chase-Lev work-stealing deque, as implemented in the Saturn library. We show that it features a subtle external and future-dependent linearization point. To deal with it, we introduce new abstractions for reasoning about prophecy variables in Iris.