Shared-memory concurrency is difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classic algorithms are epistemic: a thread enters a critical region only when, from its local view, it can rule out that another thread is concurrently in that region. We make such arguments explicit by introducing a past-time temporal epistemic logic interpreted over interleaving executions with perfect-recall local histories. Past-time operators support "since" reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give semantics and a sound proof system, instantiate the logic to a simple shared-memory language with instrumented read/write observations, and illustrate the approach on Peterson's mutual exclusion algorithm by proving a local knowledge condition that implies mutual exclusion.

翻译：共享内存并发性难以推理，因为每个线程都在其他线程的干扰下执行。与此同时，许多经典算法的正确性论证具有认知属性：仅当线程从其局部视角能够排除其他线程同时处于该区域时，它才会进入临界区。我们通过引入一种过去时态认知逻辑使此类论证显式化，该逻辑在具有完美记忆局部历史的交错执行上进行解释。过去时态算子支持"自...以来"的推理，而认知模态则捕捉给定线程从其自身观察历史中能够得出的结论。我们给出了该逻辑的语义与可靠证明系统，将其实例化为具有仪器化读写观察操作的简单共享内存语言，并通过证明可推导出互斥性的局部知识条件，在Peterson互斥算法上阐释了该方法。