Tracking CSP computations
Tracking CSP computations
复制标题
DOI：
10.1016/j.jlamp.2018.10.002
复制
发表时间：
2019-01-01
影响因子：
0.9
通讯作者：
Tamarit, S.
中科院分区：
文献类型：
--
作者：
Llorens, M.;Oliver, J.;Tamarit, S.
跟踪是理解和调试程序最重要的技术之一。跟踪使用户能够访问有关计算的其他隐藏信息。在并发语言环境中，由于进程执行顺序的不确定性以及同步对该顺序的限制，计算尤其复杂；因此，跟踪器是探索、理解和调试并发计算的强大工具。在CSP中，跟踪是定义特定执行的事件序列。这种跟踪概念与其他范例中使用的概念完全不同，在其他范例中，跟踪是由特定执行期间计算的源代码表达式形成的。我们把这个痕迹的第二个概念称为痕迹。在这项工作中，我们介绍了在进程代数(如CSP)中跟踪并发和显式同步计算的理论基础。在这类系统中跟踪计算是一项困难的任务，因为底层操作语义的微妙结合了并发性、不确定性和非终止性。我们定义了一种仪表化的操作语义，其副作用是生成可用于跟踪计算的适当数据结构(跟踪)。跟踪语义的形式化定义提高了对跟踪过程的理解，也使我们能够形式化地证明计算出的跟踪的正确性。(C)2018 Elsevier Inc.保留所有权利。
Tracing is one of the most important techniques for program understanding and debugging. A trace gives the user access to otherwise hidden information about a computation. In the context of concurrent languages, computations are particularly complex due to the non-deterministic execution order of processes and to the restrictions imposed on this order by synchronizations; hence, a tracer is a powerful tool to explore, understand and debug concurrent computations. In CSP, traces are sequences of events that define a particular execution. This notion of trace is completely different to the one used in other paradigms where traces are formed by those source code expressions evaluated during a particular execution. We refer to this second notion of traces as tracks. In this work, we introduce the theoretical basis for tracking concurrent and explicitly synchronized computations in process algebras such as CSP. Tracking computations in this kind of systems is a difficult task due to the subtleties of the underlying operational semantics which combines concurrency, non-determinism and non-termination. We define an instrumented operational semantics that generates as a side-effect an appropriate data structure (a track) which can be used to track computations. The formal definition of a tracking semantics improves the understanding of the tracking process, but also, it allows us to formally prove the correctness of the computed tracks. (C) 2018 Elsevier Inc. All rights reserved.