/SMT-RT

An SMT approach for solving real-time schedulability analysis problems

Primary LanguagePythonBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

A task scheduling simulator

We implement a simple scheduler based on weakly hard scheduling method to simulate the scheduling process of multiple tasks on a single processor. The weakly hard scheduling model serves as a method for characterizing systems that can withstand certain deadline misses, which introduces (m,k) constraint to describe a task.

(m,k) constraint: no more than 𝑚 deadline misses must occur for any k consecutive activations of the task.

And we implemented the scheduler using the job-continue policy, which means the job will continue executing until its completion even if its deadline is missed.

Project Overview

The project consists of several components that work together to generate, preprocess, and validate task sets. The main parts of the project include task generation, preprocessing, initialization, and verification.

TaskSimulation/
|--task
|   |--__init__.py
|   |--generator.py
|   |--config.py
|   |--taskset_init.txt
|   |--taskset_result.txt
|--pre
|   |--__init__.py
|   |--pre.py
|   |--preProcess.c
|   |--preProcess
|--init.c
|--main.c
|--scheduler.c
|--scheduler.h
|--simulate.c
|--simulate.h
|--task.h
|--utils.h
|--utils.c
|--start.py
|--README.md

task

generator.py

  • This script generates an initial task set using the DRS algorithm. The generated tasks is saved into taskset_init.txt.

config.py

  • Parameters that can be modified:

    • NUM_TASKS: number of tasks to generate.
    • UTILIZATION_SUM: the total CPU utilization of all tasks.
    • TMIN: minimum task period.
    • TMAX: maximum task period.
    • M: the m in (m, k) constraint.
    • K: the k in (m, k) constraint.

taskset_init.txt

  • This file contains tasks generated by arguments defined in config.py.

taskset_result_*.txt

  • These files contain all results of weakly-hard scheduling anlysis by CBMC and time information.

pre/pre.py

  • This script preprocesses the initial tasks from ./task/taskset_init.txt to preliminarily check if the tasks are schedulable. It updates the schedulable field of each task based on the analysis results.

  • This script also reads task information from taskset_init.txt and writes it into the initialization section of task.h.

simulate.c, main.c, simulate.h, task.h

  • These files define the process of simulation, including task scheduling and constraint checking.

start.py

  • This script initiates the verification process to check whether the tasks satisfy the given constraints.

How to use it

Generate initial tasks and initiate

  • Modify NUM_TASKS, UTILIZATION_SUM, TMIN, TMAX, M and K in ./task/config.py with the desired parameters and run the following instruct to create taskset_init.txt and initiate.
cd SMT-RT
python -m pre.pre # modify it according to the actual path.

Start checking

  • Run start.py to start verifying.
python start.py <task_index> # 'task_index' is a integer which represents a task is not schedulable, and you want to check if it meets (m,k) constraint. The 'task_index' is between 1 and the number of task in taskset.