AI 中文总结
该研究提出基于认知逻辑的并发实现信息泄露推理框架，得到多类并发对象的无信息泄露实现，明确了此类实现的可能性与局限性。
AI 中文摘要
并发对象的抽象规范确定了操作可能返回的值，同时也隐含地约束了操作可能知晓的信息，例如不影响操作结果的其他操作的参数，甚至这些操作是否发生。具体实现虽符合抽象规范，但仍可能通过内部协调机制暴露额外信息。我们提出了一种用于推理并发实现中信息泄露的框架，该框架使用认知逻辑，以抽象对象本身作为允许观察的参考，比较进程在抽象规范下可能知晓的内容与在具体实现中可能知晓的内容，由此产生多种无信息泄露实现的概念。利用该框架，我们研究了无信息泄露实现的可能性与局限性：给出了多值寄存器和有界最大寄存器的完全无信息泄露无等待实现，但证明无法用有限状态基对象无等待实现完全无信息泄露的无界最大寄存器；随后考虑较弱的保证，得到了栈、队列和近似一致的参数无信息泄露实现。这些结果表明，无信息泄露保证通常可与正确性和进展要求兼容，同时也指明了其局限性。
英文摘要
Abstract specifications of concurrent objects determine which values operations may return, but they also implicitly constrain which information operations may know, for example the arguments of other operations that do not affect their outcome, or even whether such operations occurred. Concrete implementations, while correct with respect to the abstract specification, may nonetheless expose additional information through their internal coordination mechanisms. We introduce a framework for reasoning about information leakage in concurrent implementations. The framework uses epistemic logic to compare what a process may know under an abstract specification with what it may know in a concrete implementation, using the abstract object itself as the reference for permissible observations. This yields several notions of non-leaking implementations. Using this framework, we investigate both the possibilities and limitations of non-leaking implementations. We present fully-non-leaking wait-free implementations of multi-valued registers and bounded max registers, but show that a fully-non-leaking unbounded max register cannot be implemented in a wait-free manner from finite-state base objects. We then consider a weaker guarantee, obtaining argument-non-leaking implementations of stacks, queues, and approximate agreement. These results demonstrate that non-leakage guarantees are often compatible with correctness and progress requirements, while also indicating their limitations.
CommentsFull version of the paper appearing in DISC 2026 (Best Paper Award)
