Когда использовать блокировку / разблокировку семафора и ожидание / уведомление? - PullRequest
Новая
       15

Когда использовать блокировку / разблокировку семафора и ожидание / уведомление?

0 голосов
/ 28 ноября 2018

Я изучаю Promela и использую SPIN для моделирования некоторых примеров, которые я нашел.Эта модель включает в себя симуляцию заказа еды.Таким образом, заказы клиентов, кассир принимает заказы, отправляет их на сервер, обратно к клиенту и т. Д.

Вот последовательность действий программы.

Конкретные процессы

Вот код, который я написал до сих пор: 

#define NCUSTS 3    /* number of customers */
#define NCASHIERS 1 /* number of cashiers */
#define NSERVERS 1  /* number of servers */
#define NOBODY 255

#define semaphore byte   /* define a sempahore */

/*
 * lock (down) and unlock (up) functions for mutex semaphores
 */
inline unlock(s) {s++;}
inline lock(s) {atomic{ s>0 ; s--}}

/*
 * wait (down) and notify (up) functions for signaling semaphores
 */
inline notify(s) {s++;}
inline wait(s) {atomic{ s>0 ; s--}}

mtype = {CHILI, SANDWICH, PIZZA, NULL} ; // the types of foods (added null for resets)
mtype favorites[NCUSTS];
mtype orders[NCUSTS] = NULL;

byte ordering = NOBODY;

semaphore waitingFood[NCUSTS] = 1;
semaphore cashierOpen = 1;
semaphore serverOpen = 1;

bool waiting[NCUSTS] = false;


/*
 * Process representing a customer.
 * Takes in their favorite food and an integer id
 * to represent them
 */
proctype Customer(mtype favorite; byte id)
{
    /* customer cycle */
    do
    ::

        //Enter
        printf("Customer %d Entered\n", id);

        //Record
        favorites[id] = favorite;

        //Wait for cashier
        cashierOpen > 0;
        atomic{
            lock(cashierOpen);
            printf("Cashier selects customer %d\n", id);
            ordering = id;
        }
        //Order
        orders[id] = favorite;
        printf("Customer orders %e\n", favorite);
        unlock(cashierOpen);
        ordering = NOBODY;


        printf("Customer %d is waiting for %e\n", id, favorite);
        waiting[id] = true;
        wait(waitingFood[id]);
        waitingFood[id] > 0;

        printf("Customer %d recieves food and leaves\n", id);
        favorites[id] = NULL;
        orders[id] = NULL;

    od ;
}

/*
 * Process representing a cashier
 */
proctype Cashier()
{
    do
    ::
        printf("Cashier is waiting for a customer\n");
        cashierOpen < 1;
        printf("Cashier takes the order of Customer %d\n", ordering);
        serverOpen > 0;
        printf("Cashier passes order to server\n");
    od ;
}

/*
 * Process representing a server 
 */
proctype Server()
{

    byte id;
    do
    ::
        printf("Server is waiting for order\n");
        for(id : 0..2){
            if
            ::  waiting[id] ->
                lock(serverOpen);
                printf("Server creates order of %e for %d\n", orders[id], id);
                printf("Server delivers order of %e to %d\n", orders[id], id);
                notify(waitingFood[id]);
                unlock(serverOpen);
            ::  else ->
                    skip;
            fi;
        }
    od ;

}

/*
 * Sets up processes. This model creates two
 * customers with the favorite foods PIZZA & CHILI.
 */
init{

    atomic{
        run Customer(PIZZA, 0) ;
        run Customer(CHILI, 1) ;
        run Cashier();
        run Server();       
    }
}

Очевидно, что программа работает не так, как я ожидал.Может ли кто-нибудь помочь мне понять, как использовать семафоры и когда использовать блокировки, разблокировки ждут и уведомляют здесь?

1 Ответ

0 голосов
/ 29 ноября 2018

Эта часть вашей модели должна быть изменена: 

::  waiting[id] ->
    ...
    notify(waitingFood[id]);
    ...

Когда Server освобождает waitingFood[id], Customer не сразу превращается waiting[id] в false,так что вполне возможно, что Server обрабатывает один и тот же запрос Customer более одного раза (на самом деле это очень вероятно).

Фактически, добавив следующий ltl свойство для модели: 

ltl p0 { [] (waitingFood[0] < 2) };

и затем проверка свойства подтверждает, что переменной waitingFood может быть присвоено "неправильное" значение: 

~$ spin -search -bfs t.pml
ltl p0: [] ((waitingFood[0]<2))
Depth=      10 States=       13 Transitions=       13 Memory=   128.195 
Depth=      20 States=      620 Transitions=      878 Memory=   128.195 
pan:1: assertion violated  !( !((waitingFood[0]<2))) (at depth 22)
pan: wrote t.pml.trail

(Spin Version 6.4.8 -- 2 March 2018)
Warning: Search not completed
    + Breadth-First Search
    + Partial Order Reduction

Full statespace search for:
    never claim             + (p0)
    assertion violations    + (if within scope of claim)
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  - (disabled by never claim)

State-vector 60 byte, depth reached 22, errors: 1
     1242 states, stored
        1239 nominal states (stored-atomic)
      684 states, matched
     1926 transitions (= stored+matched)
        3 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.104   equivalent memory usage for states (stored*(State-vector + overhead))
    0.381   actual memory usage for states
  128.000   memory used for hash table (-w24)
  128.293   total actual memory usage

pan: elapsed time 0 seconds

проблемный след: 

~$ spin -p -g -l -t t.pml
ltl p0: [] ((waitingFood[0]<2))
starting claim 4
using statement merging
Starting Customer with pid 2
  1:    proc  0 (:init::1) t.pml:124 (state 1)  [(run Customer(PIZZA,0))]
Starting Customer with pid 3
  2:    proc  0 (:init::1) t.pml:125 (state 2)  [(run Customer(CHILI,1))]
Starting Cashier with pid 4
  3:    proc  0 (:init::1) t.pml:126 (state 3)  [(run Cashier())]
Starting Server with pid 5
  4:    proc  0 (:init::1) t.pml:127 (state 4)  [(run Server())]
                          Server is waiting for order
  5:    proc  4 (Server:1) t.pml:100 (state 1)  [printf('Server is waiting for order\\n')]
  5:    proc  4 (Server:1) t.pml:101 (state 2)  [id = 0]
        Server(4):id = 0
  6:    proc  4 (Server:1) t.pml:101 (state 3)  [((id<=2))]
                      Cashier is waiting for a customer
  7:    proc  3 (Cashier:1) t.pml:83 (state 1)  [printf('Cashier is waiting for a customer\\n')]
                  Customer 1 Entered
  8:    proc  2 (Customer:1) t.pml:45 (state 1) [printf('Customer %d Entered\\n',id)]
              Customer 0 Entered
  9:    proc  1 (Customer:1) t.pml:45 (state 1) [printf('Customer %d Entered\\n',id)]
 10:    proc  1 (Customer:1) t.pml:48 (state 2) [favorites[id] = favorite]
        favorites[0] = PIZZA
        favorites[1] = 0
        favorites[2] = 0
 11:    proc  1 (Customer:1) t.pml:51 (state 3) [((cashierOpen>0))]
 12:    proc  1 (Customer:1) t.pml:12 (state 4) [((cashierOpen>0))]
 12:    proc  1 (Customer:1) t.pml:12 (state 5) [cashierOpen = (cashierOpen-1)]
        cashierOpen = 0
              Cashier selects customer 0
 12:    proc  1 (Customer:1) t.pml:54 (state 8) [printf('Cashier selects customer %d\\n',id)]
        cashierOpen = 0
 12:    proc  1 (Customer:1) t.pml:55 (state 9) [ordering = id]
        ordering = 0
        cashierOpen = 0
 13:    proc  1 (Customer:1) t.pml:58 (state 11)    [orders[id] = favorite]
        orders[0] = PIZZA
        orders[1] = NULL
        orders[2] = NULL
              Customer orders PIZZA
 14:    proc  1 (Customer:1) t.pml:59 (state 12)    [printf('Customer orders %e\\n',favorite)]
 15:    proc  1 (Customer:1) t.pml:11 (state 13)    [cashierOpen = (cashierOpen+1)]
        cashierOpen = 1
 16:    proc  1 (Customer:1) t.pml:61 (state 15)    [ordering = 255]
        ordering = 255
              Customer 0 is waiting for PIZZA
 17:    proc  1 (Customer:1) t.pml:64 (state 16)    [printf('Customer %d is waiting for %e\\n',id,favorite)]
 18:    proc  1 (Customer:1) t.pml:65 (state 17)    [waiting[id] = 1]
        waiting[0] = 1
        waiting[1] = 0
        waiting[2] = 0
 19:    proc  4 (Server:1) t.pml:103 (state 4)  [(waiting[id])]
 20:    proc  4 (Server:1) t.pml:12 (state 5)   [((serverOpen>0))]
 20:    proc  4 (Server:1) t.pml:12 (state 6)   [serverOpen = (serverOpen-1)]
        serverOpen = 0
                          Server creates order of PIZZA for 0
 21:    proc  4 (Server:1) t.pml:105 (state 9)  [printf('Server creates order of %e for %d\\n',orders[id],id)]
                          Server delivers order of PIZZA to 0
 22:    proc  4 (Server:1) t.pml:106 (state 10) [printf('Server delivers order of %e to %d\\n',orders[id],id)]
 23:    proc  4 (Server:1) t.pml:17 (state 11)  [waitingFood[id] = (waitingFood[id]+1)]
        waitingFood[0] = 2
        waitingFood[1] = 1
        waitingFood[2] = 1
spin: trail ends after 23 steps
#processes: 5
        favorites[0] = PIZZA
        favorites[1] = 0
        favorites[2] = 0
        orders[0] = PIZZA
        orders[1] = NULL
        orders[2] = NULL
        ordering = 255
        waitingFood[0] = 2
        waitingFood[1] = 1
        waitingFood[2] = 1
        cashierOpen = 1
        serverOpen = 0
        waiting[0] = 1
        waiting[1] = 0
        waiting[2] = 0
 23:    proc  4 (Server:1) t.pml:11 (state 14)
 23:    proc  3 (Cashier:1) t.pml:84 (state 2)
 23:    proc  2 (Customer:1) t.pml:48 (state 2)
 23:    proc  1 (Customer:1) t.pml:18 (state 21)
 23:    proc  0 (:init::1) t.pml:129 (state 6) <valid end state>
 23:    proc  - (p0:1) _spin_nvr.tmp:2 (state 6)
5 processes created

Вот несколько дополнительных комментариев, основанных на чтении вашей модели:

  • Для Customer бессмысленноподождите cashierOpen > 0, потому что это уже сделано внутри lock(cashierOpen);

  • Факт наличия только одной переменной ordering означает, что ваша модель может отображать неверную информацию, как только cashierOpen инициализируется значением > 1

  • Customer должно выпустить cashierOpen с unlock(cashierOpen) и установите ordering в NOBODY в операторе atomic { }.Иначе какой-нибудь другой Customer мог бы записать внутри ordering между двумя инструкциями, и тогда первый Customer неправильно перезапишет такую ​​переменную с помощью NOBODY.

  • Массив waitingFood[NCUSTS] инициализируется до 1.Мне непонятно, что вы ожидаете, когда напишите wait(waitingFood[id]), поскольку в ячейке памяти уже должно быть 1, и, таким образом, Заказчику не нужно ждать.Вместо этого я думаю, что массив должен быть инициализирован в 0, и, возможно, также стоит обновить его имя, чтобы отразить это изменение.

  • Снова, запись waitingFood[id] > 0 после wait(waitingFood[id]) кажется не только бессмысленным, но и в этом случае некорректным.На этом этапе семафор должен содержать 0/1 значений!Когда wait(waitingFood[id]) может получить семафор, ячейка памяти waitingFood[id] устанавливается на 0, поэтому строка waitingFood[id] > 0 навсегда заблокирует Customer.Единственная причина, по которой сейчас этого не происходит, заключается в том, что ошибка , которую я подчеркнул в начале этого ответа, позволяет Server обслуживать один и тот же Customer несколько раз.

...