操作系统进程管理之哲学家就餐问题
OS process management conerning Dining Philosopher
2770字
2019-01-14 15:23
82阅读
火星译客

As an extension of the Dining Philosopher problem, the Driving Philosophers problem touches upon a new type of resource sharing. Owing to its applicability (egg, some applications in operating system), the Driving Philosophers problem has attracted a lot of interest in research. Maneuverability of processes (philosophers) may pose new possibilities of deadlock and starvation in such problems, so corresponding detection is very important. At first, reasonable hypothesis and simplification are adopted to apply the original formal methods in the Driving Philosophers problem in a simpler way. After that, this model and the concurrency control within the model are described in CSP. In this paper, PAT is employed to realize this model and to define a number of items to be detected.

由于它的实用性,例如在操作系统中的某些应用,哲学家开车问题如今引起了广泛的研究兴趣。这类问题由于进程(哲学家)的机动性,导致了新的造成死锁和饿死的可能,因此相应的检测便十分重要。我们首先对这一类问题做了合理的假设和简化,使得用现有的形式化方法能够简单有效地应用于哲学家开车问题。然后我们使用了CSP描述了这一模型以及其中的并发控制。本文着重于使用PAT实现这一模型,并用PAT定义了一系列需要检测的内容。

The Driving Philosophers problem, as a new type concerning process synchronization, has generalized the Dining Philosophers problem. In this problem, the philosopher number and the resources for the philosophers are unknown. What definite is that resources for each philosopher is sequentially ordered. Here, all the resources take after a round-about form in reality. Compared with reality scene, this problem resembles the problem of driving at a round-about.

哲学家开车问题是一类新的进程同步问题,它将哲学家进餐问题进行了一般化。在这个问题中,哲学家的个数是未知的,并且他所需要的资源也是未知的。可以确定的是,每个哲学家所需要的资源都是连续的并且有序的。这里,资源的形式是近似的。那么,类比于现实场景,这个问题与转盘路口的汽车驾驶问题具有相似之处。

For process synchronization, this type of problem bears a significant value in practice. As a result, the nature of this problem and other relevant problems it evoked have arouse a lot of interest in research. Basically, a resource can not be occupied synchronously by two different philosophers just like a parking space can not accommodate two cars at the same time. Aside by, equality for all philosophers should be guaranteed lest a philosopher could not dine in circumstances without deadlock. Common properties do exist between the Driving Philosophers problem and the Dining Philosophers problem, but the former problem has peculiar features. For example, traffic jam is an exclusive case for the Driving Philosophers problem. There are solutions for clearing up deadlock, not a few but complex. Consequently, deadlock prediction is of great significance.

在进程同步的情况中,这一类问题也具有相当的现实意义。因此,它的性质,以及这些性质所带来的一些需要解决的问题就成了大家关注的研究课题。基本地说,一个资源不能同时被两个不同的哲学家所占有,就像一个空间不能同时被两辆车所占据。另外,我们应当保证,系统对于哲学家的公平,即不应该有在不发生死锁(deadlock)的情况下而某哲学家无法开车。当然,哲学家开车问题有它与哲学家就餐问题的共性, 也有它的个性。例如,交通阻塞就是它独有的一个死锁情况。解决死锁往往有多种策略但却十分复杂,所以死锁情况的推测很重要。

CSP and PAT have played a great role in assistance to our project. As a powerful formal specification tool in modeling synchronization problems, CSP has paved the way for transforming the project problems from natural language to mathematical description. Using CSP# language, PAT enables us to implement the model in a real sense and facilitates a straightforward understanding of the model nature with its verification and simulation functions. This has offered much convenience to us in improving the model.

CSP和PAT为我们的项目提供了有力的帮助。首先,CSP对于同步问题的建模有着强大的形式化的描述方法。CSP为我们的项目从自然语言描述到数学形式描述铺设了桥梁。PAT使用CSP#作为语言,不仅仅让我们真正的实现了这一模型,其验证和仿真的功能使我们对模型的性质一目了然,方便了我们对模型的改进。

This paper is constructed in the following way: Section 2 elaborated the Driving Philosophers problem, details of philosopher and resource, reasonable hypothesis and comparison with the Dining Philosophers problem. Section 3 introduced basic syntax and semantics of CSP and PAT’s programming environment. Section 4 described the modeling of the Driving Philosophers problem. Section5 told about how to implement the Driving Philosophers problem in PAT. Section 6 listed the conclusions tested in PAT as well as the analysis of such conclusions. Section 7 recorded some features of the integrated PAT environment from user’s perspective and provided some suggestions for improvement.

本文是这样组织的:第 2 节详细介绍了哲学家就餐问题 , 给出了哲学家和资源的细节以及我们做出的合理的假设,并将其与哲学家就餐问题 作了比较。第 3 节介绍了的基本的语法语义和PAT的编程环境。第 4 节使用DFA对哲学家开车问题进行建模。第 5 节 详细阐述了如何在PAT中对哲学家开车问题进行实现。 第 6 节列出了使用PAT验证的结论并对其进行了分析。 第 7 节从用户角度记录了PAT这一集成环境的一些特性并提出了改进意见。

CSP, recognized as the ideological basis of distributed process and concurrent language coming into view later, is a symbol set used to describe interactive targets, especially for extensive systems. Exactly, CSP is a language for describing parallel agent systems communicating via messaging.

CSP,被认为是后来的分布式进程及并发语言的思想基础,是一种描述交互的符号,可以用来描述大范围系统。更确切的说,是一种用来描述通过传递消息来进行通信的并行代理系统的符号。

Start state: No resource is occupied at this moment.

初始状态:此时还未占领任何一个资源。

Occupying state: Once a philosopher occupies a resource, he will shift to occupying state and keep occupying other resources until the last resource is exhausted before he shifts to next state.

占用状态:哲学家占用完一个资源后进入此状态,并不断占用资源直到占用最后一个资源后再转入下一状态。

Driving state: After the last resource is exhausted, the philosopher will shift to this state. Once the philosopher has released the first resource, he will shift to next state.

开车状态:哲学家在占用完最后一个资源后进入此状态,并在释放第一个资源后转入下一状态。

Releasing state: The philosopher will switch to this state after releasing the first resource. After that he will keep releasing the resources he occupied until the last resource is released before he shifts to next state.

释放状态:哲学家在释放第一个资源后进入此状态,并不断释放自己占有的资源直到释放完最后一个资源后转入下一个状态。

End state: After releasing the last resource, the philosopher will shift to this state and return to its initial state. Therefore, seen from the implementing perspective, there is no essential distinction between the start state and the end state.

终止状态:哲学家在释放完最后一个资源后进入此状态,并自动转入初始状态,因此在实现中,初始状态和终止状态并没有实际的区别。

Start state and end state have been described in Section 4.1, so repletion is unnecessary here.

初始状态与终止状态和4.1中的描述相同,在此不再赘述。

Occupying state:The philosopher will enter this state after occupying the first resource and will leave this state after occupying next resource.

占用状态:在哲学家占用完第一个资源后进入此状态,并在哲学家占用下一个资源后离开此状态。

Driving state:When a philosopher occupies two resources at the same time, he will keep driving for a while and then release the resources occupied before he shift to next state.

开车状态:当一个哲学家同时占用两个资源后,则他开了一段路程的车后释放其已使用的资源并进入下一个状态。

Releasing state:When a philosopher needs to move forward after releasing a resource and shifting to releasing state, he should return to occupying state; or he will shift to end state before releasing the last resource.

释放状态:当一个哲学家释放一个资源后进入此状态,如果哲学家还需要前行,则其返回至占用状态;否则释放最后一个资源并进入中止状态。

Resource alternates its state between available and occupied. Once occupied by a philosopher, the resource will switch from available state to occupied state; when released by a philosopher, the resource will switch from occupied state to available state;

资源在两个状态之间相互转换,当其被某个哲学家占用后,则由“可用”状态转向“占用”状态;当其被某个哲学家释放后,则由“占用”状态转向“可用”状态。

In Figure5-1, we defined the philosopher number as variable N and the resource number as variable M. Here we assign 2 to N and 6 to M.

在图 5-1中,我们定义了哲学家的个数以及资源的个数。其中,N表示哲学家的个数,M表示资源的个数。在这里,我们有2个哲学家和6个资源。

In Figure5-2, we defined the start point and end point of resources needed by all philosophers. For event, the start point and the end point of the resources needed by philosopher 2 is respectively 4 and 1, then the sequence of the resources he needed comes to be {4,5,0,1}. 

在图 5-2中,我们定义了所有哲学家所需要的资源的起始点和终止点。例如,哲学家2所需要的资源的起始点为4,终止点为1,那么他所需要的资源按顺序是{4,5,0,1}。

In Figure5-3, we defined an array started and with a length of 2N, of which started [2i] represents the start resource needed by the i-th philosopher and start_end [2i +1] represents the end resource needed by the i-th philosopher. This is to facilitate generalized modeling for the philosopher process.

在图5-3中,我们定义了一个长度为2N的数组 started,其中started[2i]表示第i个哲学家的起始资源,start_end[2i+1]表示第i个哲学家的终止资源。其目的是为哲学家进程的一般化建模提供方便。

In Figure5-4, the i-th element of the array pointer is used to indicate the resource a philosopher currently applying for. The initial value of each element is set to the start point of the resources applied by their corresponding philosopher.

在图5-4中,数组pointer中的第i个元素被用来指示第i个哲学家当前需要申请占用的资源。每个元素的初始值被设置为相对应哲学家所需占用资源的起始点。

In Figure5-5, the array flag is used to identify the status of the corresponding philosopher. Flag [2i] = 0 means that the i-th philosopher has not yet “driven”; flag [2i] = 1 means the i-th philosopher has “driven” already; Flag [2i +1] = 0 means that the i-th philosopher has not yet occupied all the resources he needed; Flag [2i +1] = 1 means that the i-th philosopher has already occupied all the resources he needed. This array, serving as a pre-condition in modeling the philosopher processes, is used to identify the philosopher's next movement.

在图5-5中,数组flag用来标识相应哲学家的状态。flag[2i]=0时,表示第i个哲学家还没有开车, flag[2i]=1时,表示第i个哲学家已经开车了;Flag[2i+1]=0时表示第i个哲学家还未占满所需的全部资源,Flag[2i+1]=1时表示第i个哲学家已经占满所虚的全部资源。此数组在哲学家进程建模中作为前置条件来标识哲学家的下一步动作。

In Figure5-6, the array count is used to record the “drive” number of each philosopher, and sum is used to record the total “drive” number of all philosophers. To prevent starvation, these two variables are mainly used in situations absent of deadlock.

在图5-6中,数组count用来记录每个哲学家当前开车的次数,sum用来记录所有哲学家开车的总次数。这两个变量主要是用来在没有死锁的情况下防止饿死。

In Figure5-7, the resource array is used to record the current occupation of a resource; resource [i] = m means the i-th resource is shared by m philosophers at the same time. This variable is only used to test whether a resource conflict will occur in the system.

在图 5-7中,数组resource用来记录当前某个资源被占用的情况,resource[i]=m表示第i个资源在某一状态同时被m个哲学家共享。这个变量只用来测试系统能否到达占用资源冲突的状态。

In Figure5-8, mutex is used to identify whether the system will encounter conflict (two philosophers share the same resource simultaneously); mutex = true means that the system will encounter a conflict.

在图 5-8中,mutex用来标识系统能否达到冲突的状态(两个哲学家同时享用一个资源),mutex=true表示系统能够达到冲突的状态。

In Figure5-9, we define all the processes for each philosopher. The processes are known as “occupy a resource”, “drive” and “release a resource”.

在图5-9中,我们总体定义了每个哲学家存在的执行过程,对于每个哲学家基本有三个步骤:占用资源;开车;释放资源。

Precondition is used to guarantee equality. In the absence of deadlock, the precondition can exempt any philosopher from being starved.

前置条件的作用是为了达到公平性,在没有死锁的情况下,前置条件可以保证没有一个哲学家被饿死。

In Figure5-10, the entire process of resource occupation is described in perspective of individual philosopher. Similarly, the process of resource release is also expressed in perspective of individual resource. Next, we model in detail for an event in which a certain resource is occupied by a certain philosopher.

在图 5-10中,我们将哲学家占用资源的整个阶段表述成该哲学家对每个具体资源的占用。同样,对资源的释放也表述成对每个具体资源的释放。接下来,我们对某个哲学家占用某个资源的过程进行详细建模。

In Figure5-11, in-detail modeling of event in which the k-th resource is occupied by the i-th philosopher is given. The precondition guarantees: (1) there is still other resource to be occupied by the i-th philosopher; (2) the i-th philosopher has not yet completed “drive”; (3) the k-th resource is the exact one the i-th philosopher wants to occupy for the moment.

在图 5-11中,我们对第i个哲学家占用第k个资源进行了详细建模。前置条件保证1.第i个哲学家还有资源需要占领;2.第i个哲学家没有完成开车动作;3.保证第k个资源是第i个哲学家当前所需要占用的资源。

There are three events in this process: once the i-th philosopher has entered k-th resource (enter.i.k), each identifier must be updated (tau event); the k-th resource is not occupied in the real sense until each identifier has been updated (occupied.i.k). In semantics view, enter.i.k and occupied.i.k are of the same event. They are divided into two independent events for reflecting the update process.

在这一过程中有三个事件:当第i个哲学家进入第k个资源(enter.i.k)后,必须对各个标识量进行更新(tau事件),在更新完毕后才表明第i个哲学家真正占用了第k个资源(occupied.i.k)。从语义上说,enter.i.k与occupied.i.k其实是一个事件,但为了表述出其中更新的过程,故在此拆成两个独立的事件。

In Figure5-12, we provide in-detail modeling for the event in which the i-th philosopher released the k-th resource.

在图 5-12中,我们对第i个哲学家释放第k个资源进行了详细建模。

The precondition guarantees: (1) the i-th philosopher has completed driving; 2. the k-th resource is the exact one the i-th philosopher wants to release.

前置条件保证了1.第i个哲学家已经完成了开车;2.第k个资源是第i个哲学家当前所需要释放的资源。

Similar to the process of occupying resources, three events in this process must be fulfilled: when the i-th philosopher has released the k-th resource (exit.ik), each identifier must be updated (tau event). the k-th resource is not released in the real sense until each identifier has been updated (occupied.i.k). Seen from semantics perspective, exit.ik event and released.ik events are of the same.

与占用资源的过程相同,在这一过程中同样需要三个事件:当第i个哲学家释放第k个资源(exit.i.k)后,必须对各个标识量进行更新(tau事件),在更新完毕后才表明第i个哲学家真正释放了第k个资源(occupied.i.k)。同理,从语义上说,exit.i.k与released.i.k是同一事件,在此不在赘述。

In Figure5-13, we modeled the drive process for the i-th philosopher in detail.

在图 5-13中,我们对第i个哲学家开车进行详细建模。

Precondition guaranteed: 1. the i-th philosopher has not yet driven; 2. the i-th philosopher has occupied all the resources he needs

前置条件保证了:1.第i个哲学家还未进行开车;2.第i个哲学家已经占用所有的他所需要的资源。

Events in the model are very simple, but all identifiers must be updated after the drive.i event occurred. What worth noting here is: according to specific requirement in modeling, the two counting variables of counter[] and sum must be cleared. Why clear is needed here? Because: 1. Without the clear operation, runtime error will occur in system operation; 2. Clear operation will speed up the system verification; 3. Optional clear adds flexibility of the system model.

模型中的事件很简单,但在drive.i事件后我们同样需要对各个标识量进行更新。这里需要的注意的是:根据模型的具体需求,需要在某一状态将counter[]和sum这两个计数器清零。其目的是为了:

1.若没有清零操作,系统在运行时将错误;

2.清零操作有助于提高系统的验证速度;

3.自行决定清零条件可以使系统模型更加灵活。

In Figure5-14, we model for resource thread. Event is required to be sequentially ordered. The k-th resource can be occupied and released by any philosopher, but this resource can not be occupied by any other philosopher until the philosopher has released it. This indirectly ensures that no resource is simultaneously occupied by two different philosophers.

在图 5-14中,我们对资源线程进行了建模。规定了其事件是时序上的顺序性要求。对以第k个资源,他可以被任意一个哲学家占有和释放,但在被某个哲学家释放以前不能被另一个哲学家占有。这间接的保证了没有一个资源不同时被两个不同的哲学家占有的情况的发生。

In Figure5-15, the entire system modeling is done. To achieve this, all the philosophers and the resources are synchronized.

在图 5-15中,我们对整个系统进行了建模。实现的方法是将所有的哲学家和资源进行同步。

In Figure5-16, modeling extension is conducted to the entire system. The new thread Test_mutex is used to detect whether there is any resource being shared by two philosophers. If such resource is detected, the variable mutex will be set to true, otherwise it will be set to false as its default value.

在图 5 -16中,我们对整个系统的建模进行了扩展。新线程Test_mutex主要工作是检测在原模型中是否存在两个哲学家共享同一资源的情况。如果存在将mutex设为true,否则mutex为缺省值false。

In this version, the resource modeling and multi-system modeling is fully consistent with the previous version. As to definition, slight difference exists between the two versions. Great difference lies in modeling for philosopher(s). To be precise, this section only explains the parts with different definition and modeling for philosopher(s). For other content, please refer to the previous version.

在这个版本中,对资源建模以及多系统建模与前一版本完全一致。在定义部分与上一版本有少许不同。差别比较大的是对哲学家的建模。为避免赘述,此节中只对这一版本的不同定义的部分及对哲学家的建模进行说明,其他部分可参照上一版本。

In Figure5-17, explanations on differences between the first parts of the two versions are given in the first part of this version.

在图 5-17中,我们对此版本中第一部分与上一版本的不同之处进行了说明。

The array flag_new is used to identify the responsive status of philosopher threads; Flag_new [i * 3] = 0 means that the i-th philosopher has not yet occupied the lastresource he needed; Flag_new [i * 3] = 1 means that the i-th philosopher has occupied the lastresource he needed; Flag_new [i * 3 +1] = 0 means that the i-th philosopher has more than one resource to occupy; Flag_new [i * 3 +2] = 0 means that the i-th philosopher has not yet completed driving; Flag_new [i * 3 +2] = 1 means that the i-th philosopher has completed driving already.

数组flag_new用来标识哲学家线程的响应状态。Flag_new[i*3]=0时,表示第i个哲学家还没有占用最后一个所需资源,Flag_new[i*3]=1时,表示第i个哲学家已经占用了最后一个所需资源;Flag_new[i*3+1]=0时,表示第i个哲学家需要不止1个的资源去占用,Flag_new[i*3+1]=1时,表示第i个哲学家只需要1个资源去占用;Flag_new[i*3+2]=0时,表示第i个哲学家还没有完成开车动作,Flag_new[i*3+2]=1时,表示第i个哲学家已经完成了开车动作。

In Figure5-18, we expressed all the implementation processes for each philosopher. There are four periods for each philosopher: 1. The initial stage – occupying the first resource he needed; 2. Mixing stage – occupying next resource -> drive for a while -> releasing the previous resource; 3. completing drive stage - occupying the lastresource -> completing the final stretch of drive; 4. releasing resources in the completion stage – releasing the lastresource.

在图 5-18中,我们整体表述了每个哲学家存在的执行过程。对于每个哲学家存在大体四个阶段:

1.初始阶段——占用了第一个其所需要的资源;

2.混合阶段——占用下一个资源->开车形式一段距离->释放前一个资源;

3.完成开车动作阶段——占用最后一个资源->完成最后一段开车动作;

4.完成释放阶段——释放最后一个资源。

Precondition is set for equity: In the absence of deadlock, the precondition can guarantee that no philosopher will be starved.

前置条件的作用是为了达到公平性,在没有死锁的情况下,前置条件可以保证没有一个哲学家被饿死。

In Figure5-19, we signify the occupying/releasing process of any philosopher in perspective of individual resource. Occupation of resource k, releasing of resource k-1 and a period of drive are included in the process of Phil_enter_drive_release (i, k). Specific modeling is given for these three processes below.

在图 5-19中,我们将每个哲学家占用释放的过程表示成具体的对某个资源的释放或占用。其中在Phil_enter_drive_release(i,k)进程中包括了对资源k的占有过程,对资源k-1的释放过程以及drive一段距离的过程。下面就对这些过程进行具体建模。

In Figure5-20, we model for the process in which the i-th philosopher occupied the initial resource.

在图 5-20中,我们对第i个哲学家占用初始资源的过程进行了建模。

 

Precondition is to guarantee: 1. the i-th philosopher currently needs more than one resource; 2. the i-th philosopher has not yet completed driving; 3. the i-th philosopher has not yet occupied the lastresource he needs; 4. the k-th resource is the exact initial resource the i-th philosopher needs.

前置条件保证了:

1.当前情况下第i个哲学家需要不止一个资源;

2.第i个哲学家还没有完成开车;

3.第i个哲学家还没有占用其所需要的最后一个资源;

4.第k个资源正是第i个哲学家所需要的起始资源。

In this process there are three events: once the i-th philosopher entered its initial resource (enter.ik) ; each identifier must be updated (tau event); the initial resource is not occupied in the real sense until each identifier has been updated (occupied.i.k). Analysis in the previous version shows that, in semantic perspective, enter.ik and occupied.ik are of the same event, so repeat ion is unnecessary here.

在这一过程中有三个事件:当第i个哲学家进入其初始资源(enter.i.k)后,必须对各个标识量进行更新(tau事件),在更新完毕后才表明第i个哲学家真正占用了其初始资源(occupied.i.k)。由上一版本的分析可知,从语义上说,enter.i.k与occupied.i.k其实是一个事件,这里不再赘述。

In Figure5-21, we model for the process in which the i-th philosopher released the lastresource.

在图 5-21中,我们对第i个哲学家释放最后资源的过程进行了建模。

Precondition is to guarantee: 1. the i-th philosopher has completed driving; 2. the k-th resource is exactly the lastresource the i-th philosopher wants to release.

前置条件保证了:1.第i个哲学家已经完成了开车动作;2.第k个资源正是第i个哲学家所需要释放的最后一个资源。

Similar to the process of occupying resources, three events in this process must be fulfilled: when the i-th philosopher has released the lastresource (exit.ik), each identifier must be updated (tau event); the lastresource is not released by the i-th philosopher in the real sense until each identifier has been updated (occupied.i.k). In semantics perspective, exit.ik event and released.ik events are of the same. So repletion is unnecessary here.

与占用资源的过程相同,在这一过程中同样需要三个事件:当第i个哲学家释放最后一个资源(exit.i.k)后,必须对各个标识量进行更新(tau事件),在更新完毕后才表明第i个哲学家真正释放了最有一个资源(occupied.i.k)。同理,从语义上说,exit.i.k与released.i.k是同一事件,在此不在赘述。

In Figure5-22, modeling is conducted for the process in which the i-th philosopher completed driving.

在图 5-22中,我们对第i个哲学家完成开车这一过程进行建模。

Precondition is to guarantee: 1. the i-th philosopher has not yet completed driving; 2. i-th philosopher has occupied the last resource or he needs to occupy only one resource.

前置条件保证了:1.第i个哲学家还没有完成开车;2.第i个哲学家已经占用了最后一个资源或者第i个哲学家只需要占用一个资源

Event in this model is very simple, but variables must be updated after drive.i event.

模型中的事件很简单,但在drive.i事件后我们同样需要对各个标识量进行更新。

Similarly, the two variables of sum and count need to be cleared, if necessary.

同理,适当时候需要对sum和count变量进行清零,这里不再赘述。

In Figure5-23, modeling is conducted for the i-th philosopher's mixing process of enter_drive_exit.

在图 5-23中,我们对第i个哲学家的enter_drive_exit这一混合过程进行建模。

Precondition is to guarantee: 1. the i-th philosopher has more than one resource to occupy; 2. the i-th philosopher has not yet completed driving; 3. the i-th philosopher has not yet occupied the lastresource; 4. the k-th resource is the exact resource the i-th philosopher currently wants to occupy.

前置条件保证了:1.第i个哲学家有不止一个资源需要占用;2.第i个哲学家还没有完成开车;3.第i个哲学家还没有占用到最后一个资源;4.第k个资源正是当前第i个哲学家所需要占用的。

In fact, this process contains three sub-processes known as “enter”, “drive” and “exit”. Modeling for these three sub-processes has already been discussed in detail previously.

这一过程事实上包含了进入、开车、离开三个子过程,而这个三个子过程的建模在此之前已经有过详细论述,故在此不再赘述。 

In the project, we found that speed of PAT verification are affected by many factors such as synchronization manner, number of threads, range of variables, thread structure and so forth. So we designed a number of circumstances to test the speed of PAT verification, without changing the program performance. We have equality verification (in two-Phase method) as our experimental subject. Experimental designs are listed as follows:

在项目的过程中,我们发现PAT验证的速度与很多因素有关,例如同步的方式,线程的数量,变量值的范围,线程构造的方式等等。于是,我们在不改变程序功能性的要求的前提下设计了多个场景以测试不同情况下PAT的验证速度。我们所选取的实验对象为两相法下的公平性验证。实验设计如下:

In this report, we made an analysis of the driving philosopher problem and then modeled for this problem. Property verifications were conducted with PAT for different instances within this model. Conclusions have been drawn as follows:

在这篇报告中,我们对哲学家开车问题进行了分析与建模,并针对模型的不同实例使用PAT进行了一些性质的验证,得到了如下结论:

1.     Our assumptions and abstraction are well-grounded. Reasonable results are achieved by modeling for and experiments on two-phase case and the one-by-one case.

1.      我们的假设和抽象是有根据的,通过对两相案例和逐步案例的建模和实验得到了合理的结果。

2.      Theory and experiment shows that the Dining Philosopher problem can be transformed into the Driving Philosopher problem. To be exact, the Dining Philosopher problem is a special case in the Driving Philosopher problem.

2  从理论和实验上说明了可以将哲学家就餐问题转化至一个哲学家开车问题,更确切的说哲学家就餐问题其实是哲学家开车问题的一个特例。

3.    Through observation, necessary and sufficient conditions for the occurrence of deadlock in the two-phase case are known. Any instance met deadlock in one-by-one case will unavoidably encounter deadlock in the two- phase case.

3  通过观察出现死锁的情况,给出了在两相案例中发生死锁的充要条件,同时说明了:任何一个逐步案例中发生死锁的实例必然会在双相案例中发生死锁;反之不成立。

4.     Mutual exclusion is realized by synchronization.

4   通过同步的方法达到了互斥的效果。

5.      Adoption of counter has exempted any philosopher in deadlock from being starved.

5 使用计数器的方法使得在不发生死锁的情况下没有哲学家会被饿死。

Further improvements in the following aspects are expected in further research:

在今后的研究中,我们需要在以下方面进行改进和完善:

1. Deadlock detection and deadlock settlement should be achieved.

1.      可以侦测并解决死锁的问题。

2. Improve the rules of the counter and make it more practical.

2.      改进计数器的规则,使得其更具有实用性。

0 条评论
评论不能为空