节点文献
并发实时系统的模型及其形式化
Models and Formalization of Concurrent Real-time Systems
【作者】 陈艳;
【导师】 王驹;
【作者基本信息】 广西师范大学 , 应用数学, 2008, 硕士
【摘要】 并发实时系统指多处理器环境下有实时要求的并发计算系统。本文第一章中介绍了一般实时系统的发展。实时系统领域的研究者通常考虑有周期性截止期的任务,任务调度问题是实时系统研究的重点,这一领域的研究成果包括有效的调度算法及相关定理,如著名的Liu-layland定理。在第二章中我们引入空间因素,提出了扩充的多处理器实时系统,建立了有空间限制的并发实时系统的模型。在这个模型中,每个任务Pi的运行需要一定的空间( )νi t(这个空间可以是常量或变量),但所提供的空间的总量D是有限的。在这一框架下,我们能清楚地刻画并行和并发,而且能获得有效的调度算法。在第三章中我们讨论并行模型,运用时段演算、分离逻辑的语言给出并行模型的形式化描述。若对(?)i , (1≤i≤m),νi(t)都是关于t的常数函数,即,我们得到了一个并行模型。Pi的空间需求为。引入空间可分离的概念:,如果∑rj≤1,j∈Δ,则Δ称之为空间可分离的,记为Δs。记,考虑一个分段函数f (t), f (t)满足对。每一个已给定的f (t)将时间轴上的每个时间段与一个可空间分离的任务集对应。即每个给定的f (t)以及相应的fi(t)对应了一个任务调度表。由此得到如下定理:定理3.1对于实时并行模型,存在一个有效调度的充要条件是存在一个定义在[ 0,1]的分段函数F ( t )使得:且对,定义在第四章中我们讨论并发模型。当任务Pi占用的空间vi ( t )是变量时,我们就得到并发模型。建立简单的并发模型LCM:令|D|=1,k是一个固定的正整数,且k≥2。对每个是Pi在第j个请求周期内的运行时段, j∈H。假设对每个Pi ,在时间段内从不间歇。vi (t)是如下定义的动态函数:Pi在时段内的时空占用量定义为,我们的目标是找到一个有效的算法使时空利用率rat尽可能大。考虑下面一个算法(贪心算法):①当t = 0时,我们在开始时刻运行k个任务。②每个进程一旦运行就直至完成才结束。③当且仅当1k的空间被释放,我们才让另一个任务切入进来并开始运行。我们采用MAPLE环境编程。根据程序输出的结果,猜测LCM在贪心算法的调度下,时空利用率的上界是。由此提出猜想:定理4.1对于并发模型LCM,是任意一个有效的调度算法∑( t)的时空利用率的上界。鉴于贪心算法将导致复杂的并发进程控制,我们提出了循环算法:①当t = 0,仅让一个任务P1运行。②当时, n是正整数,0 < n < 2 k-1,开始一个新的任务Pn +1。③当t = 1时,任务P1的进程结束,且正好有1k的空间空余出来,同一时刻任务P1的进程再次被切入,将所有空间填满。④当时, n是任意正整数,恰有一个进程结束,并有k1的空间空余出来,使得一个新的任务切入。受循环算法启发,尝试以进程代数的语言给出一种简单的时间自动机的形式化描述。
【Abstract】 In our understanding, a real-time system is a computational system with real-time requirements.We first introduce the development of general real-time system In chapterⅠ. Researchers in the real time system mainly consider the scheduling problems on the periodical processes (tasks) with periodical deadlines. The results in this area include valid scheduling algorithms under the framework that there is only one processor, theorems on algorithm discussions such as the famous Liu-Layland theorem.In chapterⅡ, we introducing the space factor and multi-processors, present an extended framework of real-time systems. Each process needs a certain amount of space, sayνi ( t). It is a real value function of the time variable t. But in the general, the total amount of space, D, is limited. In this extended framework, the parallel and concurrent processes can be clearly interpreted and the valid algorithms can be established.In chapterⅢ,we define parallel models : when (?) i ,(1≤i≤m) ,νi( t) is a constant function of t , i.e. (?) d i∈(?),ν(i t) = di. We use the language of duration calculus and separation logic to present the formalization of this parallel models . We introduce the concept of space separation of processes. Assume that for each process Pi , the ratio of its space requirement is ri= dDi. Denote a subset of {1 ,2, , m} asΔ. if∑r j≤1,j∈Δ, then we call it space separable. There are finitely many of them, we denote each of them asΔs , s∈I. We writeεs=∑r j, j∈Δs for each such a subset. Consider a step function: obtain the following theorem:Theorem 3.1For the given parallel model, three is a valid scheduling algorithm if and only if there is a step functionIn chapterⅣ,we define concurrent models ,and use the language of process algebra to present the formalization of this concurrent model. When the space occupancy function vi ( t ) is variable for each i , we obtain concurrent models of real-time processes. In this paper, we construct a basic concurrent model LCM (Linear Concurrent Model): Let D = 1, k≥2 is a fixed integer, for each Pi ,the time interval of this process being processed in the jth periodical time requirement. We also assume that for each process, when it starts to be processed, it will not stop until the process has been completed. The space occupancy function is defined as following for each i:We also define the time-space occupancy for each process over the time interval vi t.Our goal is to find algorithms in this model that the efficiency ratio is much larger than 12 . Consider the following“greedy algorithm”:1. When t = 0, we start processing k processes simultaneously.2. Each process will not stop until it has been completed.3. Whenever an amount of free space has been released, we start a new process.To understand the possible maximal time-space efficiency of this greedy algorithm, and to see the cutting points of this scheduling, we use MAPLE to make a program. Base on this grogram, we had made the conjecture that the time-space efficiency rate of greedy algorithm is . This experiment leads to the following theorem:Theorem 4.1In this concurrent model LCM, is the maximal up-bound of the time-space efficiency rates of valid scheduling algorithms.But the above program also shows that the control of the greedy algorithm is complicated. Therefore we have designed a simple cyclic algorithm with the same efficiency rate:1. When t = 0, we start only one process, say P1 .2. When , n is an int eger, 0 < n < 2 k- 1, we start a new process Pn +1 .3. When t = 1, P1 has just being finished, and the total amount of free space is just k1 , we can start P1 again so that the whole space is totally occupied.4. When , n is an integer, one process is just being finished, we can start another process.It is shown in this paper that the time-space efficiency rate of this algorithm is also .
【Key words】 Concurrent real-time systems; time-space occupancy; time-space efficiency rate; duration calculus; separation logic; process algebra;
- 【网络出版投稿人】 广西师范大学 【网络出版年期】2008年 09期
- 【分类号】TP311.52
- 【被引频次】4
- 【下载频次】152