Prioriy Ceiling Protocol
------------------------

Description:

Only uniprocessor systems are considered. A real-time application is modeled as a
finite set of tasks that run concurrently on a single processor. A task consists
of a succession of jobs, each requiring a finite amount of computation. In other
words, the computation associated with each job should terminate. Each task is
characterized by its priority, period, and by the amount of processing it requires.  
For example, a process sampling an input signal at frequency of 100 Hz can
be modeled as a periodic task of period 10ms. The successive jobs of this task
are released at time t_0, t_0 + 10ms, t_0 + 20ms, and so forth, and the
length of each job is the amount of time required for processing a single sample.

Other resources than the processor are shared by different jobs. For instance,
the jobs may share common I/O channels or communicate with each other via
shared variables. Access to these shared resources is controlled by binary
semaphores which ensure mutual exclusion. The operations for requesting and
releasing the lock on a semaphore S are denoted by lock(S) and 
unlock(S), respectively.

Each task and job has fixed priority; the priority of a job is the priority
of the task to which it belongs. Jobs are executed in priority order: if two
jobs of different priorities are ready to run at the same time, then the one
with highest priority is allocated the processor. It is wise to note that
different tasks may have the same priority, although priority assignment
techniques such as the rate monotonic or the deadline monotonic approaches
avoid this situation by giving different priorities to different tasks.

When synchronization primitives, such as semaphores, are used, there is
a problem called priority inversion which causes low priority jobs
to prevent higher priority jobs from running. For instance, a job j can
be blocked when trying to lock a semaphore S if a job k of lower priority
has locked S before j was dispatched. As a result, a job j of top
priority can be unable to execute and a job k of lower priority than j
can become active. This phenomenon may block j for long periods of time,
since other jobs, with priority greater than k, may prevent k to execute
and consequently to unlock S. So, the high-priority job j can then be
delayed by the low-priority job k that locks S but also by any job of
intermediate priority that might preempt k. Since high-priority jobs are
usually the most urgent and may have tight deadlines, such unrestricted 
priority inversion can be disastrous. In the Priority Ceiling Protocol,
the following approach is used to cope with this problem:

- Each semaphore S is assigned a fixed ceiling which is equal
to the highest priority among the jobs that need access to S.
- A job j executing lock(S) is granted access to S if the 
priority of j is strictly higher that the ceiling of any semaphore locked
by a job other than j. Otherwise, j becomes blocked and S is not
allocated to j.

A set of SAL contexts defines the basic concepts used to build the protocol model.
These contexts introduce types to represent tasks, jobs, semaphores, and priorities.
The scheduler is modeled as a SAL module which represents a state machine. The protocol
model is parametric, allowing us to experiment with different execution environments.

*** Tasks ***

The scheduler manipulates tasks that consists of a succession of jobs, each requiring a
finite amount of computation. Tasks are modeled in the context `pcp-task'. This
context contains two parameters:

- Semaphore : TYPE - the representation of semaphores. The actual value of
this parameter is usually a subrange type or a scalar type.
- NumberOfTasks : nat - the number of tasks that run concurrently.

The type TaskDescriptor describes the characteristics of a task that will be manipulated
by the scheduler. The field semaphores contains the set of semaphores used by
a task. It is important to notice that we are using the context `set'
that specifies set of elements of a given type, and provide several functions to manipulate these 
sets. The function ceiling(s, t) computes the ceiling of the semaphore s. associated
with the array of task descriptors t. The ceiling of the semaphore s is equal
to the highest priority among the tasks that need access to S. 

*** Resources ***

Our model contains a resource management component that stores the set of semaphores
allocated to or requested by each job. This component is a record of type RSRC.
This type and associated functions is described in the context `pcp-rsrc'.
This context contains three parameters:

- Semaphore : TYPE - the representation of semaphores. The actual value of
this parameter is usually a subrange type or a scalar type.

- NumberOfTasks : nat - the number of tasks that run concurrently.

- TaskDescriptors : TaskDescriptors - an array of TaskDescriptor, that
is, a description of the tasks that will be processed by the
scheduler. This information is necessary, since we need to know the
priority of each task, and the ceiling associated with each semaphore
to specify some functions in the context pcp-rsrc.

Given a job j and a resource allocation object r, r.alloc[j] is the set
of semaphores allocated by j in r, and r.request[j] is the set of
semaphores that j requested but not obtained. This set is empty unless j has
failed to aquire a lock on a semaphore.

The function blk(r, j) computes the set of jobs other than j that own 
a semaphore of ceiling as high as j's priority. These jobs will block j if j
ever tries to lock a semaphore.  As defined by function blocked, a job 
j is then blocked in r if both blk(r, j) and request(r, j) are
nonempty. This context also defines the function ceiling with only
one parameter. This function is basically an alias to the ceiling function
defined in the context pcp-task with the second parameter fixed.

Four operations control semaphore allocation and deallocation:

- alloc_step(r, j, s) executes command lock(s) on behalf of j.
  The semaphore s is allocated to j if blk(r, j) is empty; otherwise,
  s is stored in r.request[j] and j becomes blocked.
- release_step(r, j, s) execute command unlock(s) on behalf of j.
  It simply removes s from the set of semaphores allocated to j. After this
  operation, some jobs that were blocked by j may be no longer blocked. The 
  operation has no effect if j does not own s.
- release_all_step(r, j, s) releases all semaphores allocated to j. 
  It simply makes r.alloc[j] equals to the empty set.
- wakeup(r, j) allocates to j all the semaphores j requested. This
  operation is intended for a job j that is reactivated after having been
  blocked.      

As far as the priority ceiling protocol is concerned only two classes of commands
are relevant, namely, the instructions lock(s) or unlock(s) for 
requesting and releasing semaphores. The instruction unlock_all(s) is also
considered in our model. We also use a fourth class of commands representing
any other instruction performed in one step. These four classes of commands are
represented in our model by the following functions: lock, unlock,
unlock-all, and step. 

*** Scheduler ***

The scheduler is represented as SAL modules.  The scheduler selects
one job to be executed based on the available resources, that is, a
RSRC object, the status of each user job, and the dispatch table.

The time counter should be incremented with every transition, but
this approach will produce an infinite state space. However, it is
easy to see that it is sufficient to keep the time counter in
the interval [0, lcm], where lcm is least common
multiple of the periods of each task. For instance, suppose that
we have three tasks with periods: 5, 8, and 10; then it is sufficient
to keep the time counter in the interval [0, 40). The function
adjust is used to enforce this condition.  

The Turn datatype is used by the scheduler to sign which process
will execute in the current step. The function turn? basically
checks if it is the turn of a given job.

The scheduler is described in the context `pcp_scheduler'.  The output
variable dispatch stores the next dispatch time of each job.  The
output variable turn is used to select which job will be activated in
a given step. The input variable rsrc allows the scheduler to access
information about semaphore allocation and request. The initialization
section simply sets the initial values of the output variables. The
transition section executes the following commands: 

- Updates the time counter.  

- Updates the job_state array.  

- Updates the dispatch table if necessary.

- Chooses a job to be activated. A multi-command is
used to perform a non-deterministic choice from all eligible jobs. 
If there is not a eligible job, then the idle job is activated.

Our model is parametric, and may be instantiated with different environments.

The context 'tst_pcp_generic' instantiates our parametric module for a specific
configuration.

Commands:

a) Configuration tst_pcp_generic: 3 processes and 3 semaphores

- Produce an execution trace up to depth 10

  % sal-path-finder -v 3 tst_pcp_generic system

- Prove the deadlock_free using induction 

  % sal-bmc -v 3 --induction tst_pcp_generic deadlock_free

- Prove the deadlock_free property using sal-smc (symbolic model checker)

  % sal-smc -v 3 tst_pcp_generic deadlock_free

- Prove the deadlock_free property using sal-smc and backward propagation

  % sal-smc -v 3 --backward tst_pcp_generic deadlock_free

b) Configuration tst_pcp_generic2: 5 processes and 3 semaphores

- Prove the deadlock_free using induction 

  % sal-bmc -v 3 --induction tst_pcp_generic2 deadlock_free

- Prove the deadlock_free property using sal-smc 

  % sal-smc -v 3 tst_pcp_generic2 deadlock_free

- Prove the deadlock_free property using sal-smc and backward propagation

  % sal-smc -v 3 --backward tst_pcp_generic2 deadlock_free
