CN109165089A - A kind of overload real-time system based on MaxSAT optimal solution can not preemption scheduling method - Google Patents

Abstract

The invention discloses a non-preemptive scheduling method for overloaded real-time systems based on the optimal solution of MaxSAT, comprising the following steps: (S1) determining a scheduling problem, encoding task attributes as MaxSAT hard clauses; (S2) encoding scheduling objectives as MaxSAT clause; (S3) Connect the MaxSAT hard clause obtained by (S1) and the MaxSAT clause obtained by (S2) using the conjunction operator to obtain the MaxSAT problem; (S4) Calculate MaxSAT through the MaxSAT solver The optimal solution of the problem is obtained, and the optimal scheduling scheme is obtained. Through the above solution, the present invention solves the problems of difficulty in finding the optimal solution and low efficiency in the overloaded real-time system, and finally improves the efficiency of the target task scheduling method, so that the present invention not only has strong scalability and execution efficiency, but also It also has high practical value and promotion value.

Description

A non-preemptive scheduling method for overloaded real-time systems based on MaxSAT optimal solution

technical field

The invention belongs to the field of computer application, in particular to a non-preemptive scheduling method for an overloaded real-time system based on the MaxSAT optimal solution.

Background technique

Real-time systems occupy an important position in various application fields today. The study of optimal scheduling strategies for overloaded real-time systems has a positive impact on improving system stability, and has very important theoretical significance and practical value. Under normal workloads, the classical scheduling algorithm can ensure that all tasks are completed before the deadline, but in practical applications, the system load may change due to unstable factors in the working environment. Once the system is overloaded, there will be no The scheduling algorithm can complete all tasks within the deadline, a situation known as system overload. When the overload problem occurs, if there is no suitable scheduling scheme to deal with the overload situation, the system performance will drop sharply. At present, most of the scheduling algorithms for overloaded real-time systems focus on finding approximate optimal solutions. Although they can provide more efficient scheduling schemes than classical scheduling algorithms, they cannot ensure that the output approximate solutions can be stably close to the optimal solutions. For overloaded real-time systems, Cheng et al. proposed an optimal scheduling algorithm based on Satisfiability Modulo Theories (SMT), but the SMT solver must be called cyclically, which increases the computational cost to a certain extent and reduces the solution cost. Efficiency is not conducive to large-scale promotion.

SUMMARY OF THE INVENTION

The purpose of the present invention is to provide a non-preemptive scheduling method for overloaded real-time systems based on the MaxSAT optimal solution, and the present invention solves the problems of difficulty in finding optimal solutions and low efficiency in overloaded real-time systems.

In order to achieve the above object, the technical scheme adopted in the present invention is as follows:

A non-preemptive scheduling method for overloaded real-time systems based on the optimal solution of MaxSAT, comprising the following steps:

(S1) Determine the scheduling problem, and encode the task attribute as a MaxSAT hard clause, wherein the task attribute encoding and the corresponding MaxSAT hard clause should satisfy the following rules at the same time:

first rule

When a task τ _i starts at time t or after t, then the task τ _i must start at time t-1 or after t-1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, indicating that task τ _i starts to execute after time t or t-1, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

second rule

When a task τ _i ends before time t or t, then the task τ _i must end before time t+1 or t+1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, indicating that task τ _i is completed before time t or t, _ci is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

third rule

When a task τ _i starts at time t or after t, then the task τ _i must not end at t+ _ci -1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

fourth rule

When two tasks τ _i and τ _j occupy the same processor and their execution time periods overlap, then τ _i is executed before τ _j , or τ _j is executed before τ _i , and the task attribute is encoded as the following hard sub sentence:

pr _i,j ∨pr _j,i

Among them, pr _i,j is a Boolean variable, indicating that the task τ _i is executed before τ _j ;

(S2) encoding the scheduling target as a MaxSAT clause;

(S3) The MaxSAT hard clause obtained by (S1) and the MaxSAT clause obtained by (S2) are connected by a conjunction operator to obtain the MaxSAT problem;

(S4) The optimal solution of the MaxSAT problem is calculated by the MaxSAT solver, and the optimal scheduling scheme is obtained.

Further, in the step (S1), under the premise of satisfying the four rules at the same time, the task attribute coding and the corresponding rules of the MaxSAT hard clause also include: when the task τ _j depends on the task τ _i , then the task τ _i is executed before task τ _j , encoding the task attributes into the following two hard clauses:

pr _i,j and

Among them, p _i,j are Boolean variables, t=d _i -c _i +1, c _i is the execution time of task τ _i , and d _i is the deadline for task τ _i .

Still further, in the step (S1), for the Boolean variables p _i,j that have appeared, the following MaxSAT hard clauses are generated:

where r _i +ci _{≤t≤d i -ci +1} , is a Boolean variable, ci is the execution time of task τ _{i ,} and d _i is the deadline for task τ _i .

Further, in the step (S2), the scheduling target satisfies any one of the following types, and encodes it as the corresponding MaxSAT clause:

(1) To maximize the number of tasks completed before the deadline, encode the scheduling objective as a MaxSAT soft clause:

(2) Under the premise of ensuring that all key tasks are completed, maximize the number of non-critical tasks completed before the deadline, and encode the scheduling objectives of all key tasks τ _k as the MaxSAT hard clause:

Encode the scheduling objectives of all non-critical tasks τ _l as MaxSAT soft clauses:

(3) Maximize the sum of the task weights completed before the deadline, and encode the scheduling objective as a MaxSAT weighted soft clause:

Among them, _wi represents the income obtained by completing the task τ _i .

Specifically, in the step (S3), the conjunction operator ∧ is used to connect each clause to obtain the MaxSAT problem.

Compared with the prior art, the present invention has the following beneficial effects:

(1) The present invention encodes the task attribute and the scheduling target as the MaxSAT hard clause and the MaxSAT clause respectively, connects them with the conjunction operator to obtain the MaxSAT problem, and then obtains the scheduling of the optimal solution through the MaxSAT solver According to the solution, the present invention does not need to cyclically call the solver in the process of solving the optimal solution, thereby reducing the calculation cost, improving the solving efficiency, and being suitable for large-scale popularization and application;

(2) The present invention has strong expansibility and execution efficiency, can be used to solve multi-objective optimization problems, is suitable for seeking the optimal scheduling scheme in a large-scale real-time system, and strives to obtain the maximum value in the case of system overload benefit.

Description of drawings

FIG. 1 is a flow chart of the method of the present invention.

Detailed ways

The present invention will be further described below with reference to the accompanying drawings and examples, and the modes of the present invention include but are not limited to the following examples.

Example

As shown in Figure 1, a non-preemptive scheduling method for overloaded real-time systems based on the optimal solution of MaxSAT, the specific steps of the method are as follows:

Step 1: Determine the scheduling problem, and encode the task attribute as a MaxSAT hard clause, where the task attribute code and the corresponding MaxSAT hard clause should satisfy the following rules at the same time:

(1) When a task τ _i starts at time t or after t, then the task τ _i must start at time t-1 or after t-1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, indicating that task τ _i starts to execute after time t or t-1, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

(2) When a task τ _i ends before time t or t, then the task τ _i must end before time t+1 or t+1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, indicating that task τ _i is completed before time t or t, _ci is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

(3) When a task τ _i starts at time t or after t, then the task τ _i must not end at t+ _ci -1, and the task attribute is encoded as the following hard clause:

in, is a Boolean variable, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks;

(4) When two tasks τ _i and τ _j occupy the same processor and their execution time periods overlap, then τ _i is executed before τ _j , or τ _j is executed before τ _i , and the task attribute is encoded as The following hard clauses:

pr _i,j ∨pr _j,i

Among them, pr _i,j is a Boolean variable, indicating that the task τ _i is executed before τ _j ;

(5) When task τ _i starts at time t or after t, and task τ _i is executed before task τ _j , then τ _j must be executed after τ _i is completed. The boolean variables p _i,j of , generate the following MaxSAT hard clause:

where r _i +ci _{≤t≤d i -ci +1} , is a Boolean variable, ci is the execution time of task τ _{i ,} and d _i is the deadline for task τ _i .

In the present embodiment, based on the above-mentioned rules, in the step 1, under the premise that the above-mentioned five kinds of rules are satisfied at the same time, the rules of the task attribute coding and the corresponding MaxSAT hard clauses also include:

(6) When task τ _j depends on task τ _i , then task τ _i is executed before task τ _j , and the task attribute is encoded as the following two hard clauses:

pr _i,j and

Among them, t=d _i -c _i +1, c _i is the execution time of task τ _i , and d _i is the deadline of task τ _i .

Step 2: Encode the scheduling target as a MaxSAT clause, where the scheduling target satisfies any one of the following types:

For the scheduling objective (a1): to maximize the number of tasks completed before the deadline, the scheduling objective is encoded as the MaxSAT soft clause as follows:

For scheduling objective (a2): Maximize the number of non-critical tasks completed before the deadline under the premise of ensuring that all critical tasks are completed, where:

Encode the scheduling objectives of all critical tasks τ _k as MaxSAT hard clauses:

Encode the scheduling objectives of all non-critical tasks τ _l as MaxSAT soft clauses:

For the scheduling objective (a3): maximize the sum of the task weights completed before the deadline, encode the scheduling objective as a MaxSAT weighted soft clause:

Among them, _wi represents the income obtained by completing the task τ _i .

Step 3: Use the conjunction operator to connect the MaxSAT hard clause obtained in step 1 and the MaxSAT clause obtained in step 2 to obtain the MaxSAT problem. Specifically, connect each clause with the conjunction operator ∧ to get the MaxSAT problem;

Step 4: Calculate the optimal solution of the MaxSAT problem through the MaxSAT solver. The optimal solution includes the start execution time of each task fragment, so that the optimal scheduling scheme can be obtained.

Through the above solution, the present invention solves the problems of difficulty in finding the optimal solution and low efficiency in the prior art, so that the present invention not only has strong scalability and execution efficiency, but also has high practical value and promotion value.

The above-mentioned embodiment is only one of the preferred embodiments of the present invention, and should not be used to limit the protection scope of the present invention. If the technical problem is still consistent with the present invention, it should be included within the protection scope of the present invention.

Claims (5)

1. a non-preemptive scheduling method based on the overload real-time system of MaxSAT optimal solution, is characterized in that, comprises the steps: (S1) Determine the scheduling problem, and encode the task attribute as a MaxSAT hard clause, wherein the task attribute encoding and the corresponding MaxSAT hard clause should satisfy the following rules at the same time: first rule When a task τ _i starts at time t or after t, then the task τ _i must start at time t-1 or after t-1, and the task attribute is encoded as the following hard clause: in, is a Boolean variable, indicating that task τ _i starts to execute after time t or t-1, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks; second rule When a task τ _i ends before time t or t, then the task τ _i must end before time t+1 or t+1, and the task attribute is encoded as the following hard clause: in, is a Boolean variable, indicating that task τ _i is completed before time t or t, _ci is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks; third rule When a task τ _i starts at time t or after t, then the task τ _i must not end at t+ _ci -1, and the task attribute is encoded as the following hard clause: in, is a Boolean variable, c _i is the execution time of task τ _i , d _i is the deadline for task τ _i , and n is the total number of system tasks; fourth rule When two tasks τ _i and τ _j occupy the same processor and their execution time periods overlap, then τ _i is executed before τ _j , or τ _j is executed before τ _i , and the task attribute is encoded as the following hard sub sentence: pr _i,j ∨pr _j,i Among them, pr _i,j is a Boolean variable, indicating that the task τ _i is executed before τ _j ; (S2) encoding the scheduling target as a MaxSAT clause; (S3) The MaxSAT hard clause obtained by (S1) and the MaxSAT clause obtained by (S2) are connected by a conjunction operator to obtain the MaxSAT problem; (S4) The optimal solution of the MaxSAT problem is calculated by the MaxSAT solver, and the optimal scheduling scheme is obtained. 2. the non-preemptive scheduling method of overload real-time system based on MaxSAT optimal solution according to claim 1, is characterized in that, in described step (S1), under the premise of satisfying four kinds of rules simultaneously, task attribute coding and The corresponding rules of MaxSAT hard clauses also include: when task τ _j depends on task τ _i , then task τ _i is executed before task τ _j , and the task attributes are encoded as the following two hard clauses: pr _i,j and Among them, p _i,j are Boolean variables, t=d _i -c _i +1, c _i is the execution time of task τ _i , and d _i is the deadline for task τ _i . 3. the non-preemptive scheduling method for overloaded real-time systems based on the MaxSAT optimal solution according to any one of claims 1 to 2, characterized in that, in the step (S1), for the Boolean variable p _i that has occurred _,j , which generates the following MaxSAT hard clause: where r _i +ci _{≤t≤d i -ci +1} , is a Boolean variable, ci is the execution time of task τ _{i ,} and d _i is the deadline for task τ _i . 4. the non-preemptive scheduling method of overload real-time system based on MaxSAT optimal solution according to claim 1, is characterized in that, in described step (S2), scheduling target satisfies any one of following types, and it is coded as The corresponding MaxSAT clause: (1) To maximize the number of tasks completed before the deadline, encode the scheduling objective as a MaxSAT soft clause: (2) Under the premise of ensuring that all key tasks are completed, maximize the number of non-critical tasks completed before the deadline, and encode the scheduling objectives of all key tasks τ _k as the MaxSAT hard clause: Encode the scheduling objectives of all non-critical tasks τ _l as MaxSAT soft clauses: (3) Maximize the sum of the task weights completed before the deadline, and encode the scheduling objective as a MaxSAT weighted soft clause: Among them, _wi represents the income obtained by completing the task τ _i . 5. the non-preemptive scheduling method of overload real-time system based on MaxSAT optimal solution according to claim 1, is characterized in that, in described step (S3), adopt conjunction operator ∧ to connect each clause, obtain MaxSAT questions.