基于时态会话类型的并行复杂性分析
Parallel Complexity Analysis with Temporal Session Types
摘要：
我们研究的并发，消息传递程序的参数并行复杂性分析的问题。为了使分析局部化和组合化，它基于二进制会话类型的保守扩展，其结构化进程之间通信的类型和方向，并与直觉线性逻辑保持Curry-Howard对应关系。主要的创新是利用时间模态next（$\bigcirc A$）、always（$\Box A$）和eventually（$\Diamond A$）来丰富会话类型，以另外以精确而灵活的方式规定所交换的消息的定时。所得到的临时会话类型统一地表示诸如流的消息速率、流水线的延迟、并发队列的响应时间或fork/join并行程序的跨度之类的属性。成本模型中的分析是参数化的，演示文稿将重点放在通信成本上，作为一个具体的例子。建立健全的分析证明的进步和类型保护使用定时多集重写语义。有代表性的例子说明的范围和可用性的方法。
英文摘要：
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between processes and stand in a Curry-Howard correspondence with intuitionistic linear logic. The main innovation is to enrich session types with the temporal modalities next ($\bigcirc A$), always ($\Box A$), and eventually ($\Diamond A$), to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The resulting temporal session types uniformly express properties such as the message rate of a stream, the latency of a pipeline, the response time of a concurrent queue, or the span of a fork/join parallel program. The analysis is parametric in the cost model and the presentation focuses on communication cost as a concrete example. The soundness of the analysis is established by proofs of progress and type preservation using a timed multiset rewriting semantics. Representative examples illustrate the scope and usability of the approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
