A Print Spooler. In multitasking
operating systems, a number of tasks make requests to print files.
Often, there are not enough printing devices to satisfy all current
print requests simultaneously. Any print request that cannot be
immediately satisfied is placed in a queue awaiting printing. The part
of an operating system that deals with the administration of such queues
is known as a print spooler.
In this example we assume that the operating system can employ no more
than MaxDevs output devices and that each device has a queue associated
with it. We will also assume that each device is associated with a limit
of lines in a file which it will print. For example, an output device
that has a limit of 1000 lines of printing will be associated with a
queue that contains only files having no more than 1000 lines of text.
Print spoolers sometimes impose this constraint in order to forbid large
print jobs that may occupy slow printing devices for exceptionally long
periods. A schematic representation of a print spooler is shown in
figure.
Referring to the figure, spooler state consists of four components: the
queues of files waiting to be printed, each queue being associated with a
particular output device; the collection of output devices controlled
by the spooler; the relationship between the output devices and the
maximum file size that each can print; and the relationship between the
files awaiting printing and their size in lines. For example, figure
shows that the output device LP1 which has a print limit of 750 lines
has two files ftax and persons awaiting printing, and that the size of
the files are 650 lines and 700 lines, respectively.
The state of the spooler is represented by the four components: queues, output
devices, limits, and sizes. The data invariant has five components:
• Each output device is associated with an upper limit on print lines.
• Each output device is associated with a possibly nonempty queue of files awaiting printing.
• Each file is associated with a size.
• Each queue associated with an output device contains files that have a size less than the upper limit of the output device.
• There will be no more than MaxDevs output devices administered by the spooler.
A number of operations can be associated with the spooler. For example,
• An operation that adds a new output device to the spooler together with its associated print limit.
• An operation that removes a file from the queue associated with a particular output device.
• An operation that adds a file to the queue associated with a particular output device.
• An operation that alters the upper limit of print lines for a particular output device.
• An operation that moves a file from a queue associated with an
output device to another queue associated with a second output device.
Each of these operations
corresponds to a function of the spooler. For example, the first
operation would correspond to the spooler being notified of a new device
being attached to the computer containing the operating system that
administers the spooler.
As before, each operation is associated with a precondition and a
postcondition. For example, the precondition for the first operation is
that the output device name does not already exist and that there are
currently less than MaxDevs output devices known to the spooler. The
postcondition is that the name of the new device is added to the
collection of existing device names, a new entry is formed for the
device with no files being associated with its queue, and the device is
associated with its print limit.
The precondition for the second operation (removing a file from a queue
associated with a particular output device) is that the device is known
to the spooler and that at least one entry in the queue is associated
with the device. The postcondition is that the head of the queue
associated with the output device is removed and its entry in the part
of the spooler that keeps tracks of file sizes is deleted.
The precondition for the fifth operation described (moving a file from a
queue associated with an output device to another queue associated with
a second output device) is
• The first output device is known to the spooler.
• The second output device is known to the spooler.
• The queue associated with the first device contains the file to be moved.
• The size of the file is less than or equal to the print limit associated with the second output device.
The postcondition is that the file is removed from one queue and added to another queue.
In each of the examples noted in this section, we introduce the key
concepts of formal specification. But we do so without emphasizing the
mathematics that are required to make the specification formal. In the
next section, we consider these mathematics.
