КаталогИндекс раздела
НазадОглавлениеВперед

4. Пример: ограниченный буфер

Ограниченный буфер - конкретное представление абстрактной идеи последовательности порций. Последовательность доступна для двух параллельно выполняющихся программ: первая из них (производитель) модифицирует последовательность, добавляя на завершающей стадии новую порцию x; а вторая (потребитель) модифицирует ее, удаляя первую порцию. Первоначально последовательность пуста. Нам, таким образом, нужно два действия:

 (1) append(x: portion);

которое должно быть эквивалентно абстрактной операции

   sequence := sequence  <x>;

где <x>; - последовательность из единственного элемента - x, а обозначает конкатенацию двух последовательностей.

 (2) remove(result x:portion);

которое должно быть эквивалентно абстрактным операциям

    x := first(sequence); sequence := rest(sequence);

где first выбирает первый элемент последовательности, а rest обозначает последовательность с удаленным первым элементом. Очевидно, если последовательность пуста, операция first не определена; и в этом случае мы хотим быть уверены, что потребитель ожидает, пока производитель не сделает последовательность непустой.

Мы предположим, что время, требуемое для производства или потребления порции, больше времени, требуемого для того, чтобы добавить или удалить ее из последовательности. Мы должны поэтому создать проект, в котором и производитель, и потребитель оба могут модифицировать последовательность, но не одновременно.

Последовательность представлена массивом:

buffer :array 0. .N - 1 of portion;

и двумя переменными:

(1)  lastpointer: 0..N - 1;

которая указывает на позицию в буфере, в которую следующая операция добавления, поместит новый элемент, и

(2)  count:0.. N;

которая всегда хранит длину последовательности (первоначально 0).

Мы определяем функцию

  seq (b,l,c) =df if c = 0 then empty
                  else seq(b,l1,c - 1)  <b[l 1]>

где операция кружочка обозначает деление по модулю N. Заметьте, что если с не равно 0,

   first(seq(b,l,c)) = b[lc]

и

   rest(seq(b,l,c)) = seq(b,l,c - 1)

Теперь можно дать определение абстрактной последовательности в терминах данного представления:

   sequence =df seq(buffer, lastpointer, count) 

Менее формально, это может быть записано так:

   sequence = df <buffer[lastpointercount],
               buffer[lastpointercount1],
               ...,
               buffer[lastpointer1]>

Другим способом подачи этой информации мог бы быть пример и рисунок, который был бы даже менее формальным.

Инвариант для монитора:

    0 <= count <= N & 0 <= lastpointer <= N - 1

Имеются две причины для ожидания, которые должны быть представлены переменными условия:

    nonempty:condition;

означает, что счетчик порций больше 0, и

    nonfull:condition;

означает, что счетчик порций меньше N.

С таким конструктивным подходом к проекту, относительно легко закодировать монитор без ошибок.

bounded buffer:monitor
   begin buffer:array O..N - 1 of portion; 
         lastpointer: O..N - 1; 
         count: O..N;
         nonempty,nonfull:condition;
   procedure append(x:portion);
      begin if count = N then nonfull.wait; 
            note 0 <= count < N;
            buffer[lastpointer] := x;
            lastpointer := lastpointer  l;
            count := count + 1; 
            nonempty.signal
      end append; 
   procedure remove(result x: portion);
      begin if count = 0 then nonempty.wait; 
            note 0 < count < N;
            x := buffer[lastpointer  count];
            nonfull.signal
      end remove;
   count := 0; lastpointer := 0; 
 end bounded buffer;

Формальное доказательство правильности этого монитора относительно установленных абстракций и инварианта можно при желании выполнить методами, описанными в [13]. Однако эти методы представляются не приспособленными к последовательностями, которые рассматриваются в качестве примеров в этой статье.

Ввод и вывод с одним буфером может рассматриваться как упрощенный случай ограниченного буфера с N = 1. В этом упрощенном случае массив может быть заменен единственной переменной, переменная lastpointer избыточна, и мы получаем:

iostream: monitor
begin buffer: portion; 
      count 0..1;      
      nonmepty,nonfull:condition;
 procedure append(x:portion);
   begin if count = 1 then nonfull.wait;
     buffer := x;
     count := 1;
     nonempty.signal
   end append;
 procedure remove(result x:portion);
   begin if count = 0 then nonempty.wait;
         x := buffer;
         count: = 0;
         nonfull.signal
   end remove;
 count := O;
 end iostream;

Если физический вывод выполняется отдельным специальным каналом, то прерывание от канала можно моделировать вызовом iostream.remove(x); и аналогично для физического ввода - iostream.append(x).


НазадОглавлениеВперед
КаталогИндекс раздела