1

我正在尝试修复我的代码，我已经解决了死锁和互斥问题，但我不知道如何避免饥饿，因为在 promela (PML) 中没有监视器。有人能帮我吗？提前致谢

bool forchetta0 = false,forchetta1 = false, forchetta2 = false, 
     forchetta3 = false, forchetta4 = false;

bool want0 = false, want1 = false, want2 = false, want3 = false, want4 = false;

active[5] proctype filosofo(){
printf("Filosofo %d -> sto pensando\n",_pid);

ciclo:
if
::true -> printf("Filosofo %d -> PENSO \n",_pid);
::true -> printf("Fisolofo %d -> voglio mangiare\n",_pid); 

                          if
                            ::_pid == 0 -> atomic{(!want4 &&!want1);want0 = true;}
                                forchetta0 = true; forchetta4 = true;
                                printf("Filosofo 0 -> STO MANGIANDO\n");
                                forchetta0 = false; forchetta4 = false;
                                want0 = false;
                                printf("Filosofo 0 -> HO FINITO DI MANGIARE\n");

                            ::_pid == 1 -> atomic{(!want0 &&!want2);want1 = true;}
                                forchetta0 = true; forchetta1 = true;
                                printf("Filosofo 1 -> STO MANGIANDO\n");
                                forchetta0 = false; forchetta1 = false;
                                want1 = false;
                                printf("Filosofo 1 -> HO FINITO DI MANGIARE\n");

                            ::_pid == 2 -> atomic{(!want1 &&!want3);want2 = true;}
                                forchetta1 = true; forchetta2 = true;
                                printf("Filosofo 2 -> STO MANGIANDO\n");
                                forchetta1 = false; forchetta2 = false;
                                want2 = false;
                                printf("Filosofo 2 -> HO FINITO DI MANGIARE\n");

                            ::_pid == 3 -> atomic{(!want2&&!want4);want3= true;}
                                forchetta3 = true; forchetta2= true;
                                printf("Filosofo 3 -> STO MANGIANDO\n");
                                forchetta3 = false; forchetta2= false;
                                want3 = false;
                                printf("Filosofo 3 -> HO FINITO DI MANGIARE\n");

                            ::_pid == 4 -> atomic{(!want0 &&!want3);want4= true;}
                                forchetta4 = true; forchetta3= true;
                                printf("Filosofo 4 -> STO MANGIANDO\n");
                                forchetta4 = false; forchetta3= false;
                                want4 = false;
                                printf("Filosofo 4 -> HO FINITO DI MANGIARE\n");
                        fi;
fi;

goto ciclo;
}
4

1 回答 1

0

您的代码中的陷阱是，如果他的一个邻居已经在尝试吃饭，每个哲学家都会避免进食，从某种意义上说，他们彼此之间的行为过于礼貌，因此由调度程序决定谁会挨饿。

在意识到如果每个哲学家都是自私的并且只是尽可能多地抓住叉子之后，您可能会以这种方式设计代码，那么您最终可能会陷入僵局。

正确的解决方案存在于两个极端之中：你需要放松每个哲学家对吃饭的强烈承诺，刚好足以避免僵局，但又不能过度到饿死。

避免僵局而不引起饥饿的一种可能方法是引入利他哲学家的概念，即当意识到由于出现僵局情况而没有人可以吃东西时，会放下手中的叉子的哲学家。

为了避免僵局，只有一位 利他主义哲学家就足够了，因此所有其他哲学家都可以继续贪婪并试图抓住尽可能多的叉子。

但是，如果您在执行死刑期间从未改变谁是利他主义哲学家，那么您最终可能会被那个人饿死。因此，解决方法是无限频繁地改变利他主义哲学家 。一个公平的策略是，每当一位哲学家在陷入僵局的情况下利他行为时，就以循环方式改变它。这样，没有哲学家会受到惩罚，并且您实际上可以验证在调度程序为每个哲学家提供无限频繁执行的机会的公平条件下，没有哲学家会饿死。

为了帮助您在Promela中对这种方法进行建模，我将向您提供以下NuSMV代码，它解决了相同的问题，取自特伦托大学形式方法实验室的教材：

MODULE philosopher(ID, left_chopstick, right_chopstick, ALTRUIST, DEADLOCK)

  VAR
    state : {think, pickup, eat, putdown};

  ASSIGN
    init(state) := think;

    next(state) := case
      (DEADLOCK) & (ALTRUIST = ID): think;
      (state = think): pickup;
      (state = pickup) & (left_chopstick = 1) & (right_chopstick = 2): eat;
      (state = eat): putdown;
      (state = putdown) & !(left_chopstick = 1) & !(right_chopstick = 2): think;
      TRUE : state;
    esac;

    next(left_chopstick) := case
      (DEADLOCK) & (ALTRUIST = ID): 2;
      (state = pickup) & (left_chopstick = 0): 1;
      (state = putdown) & (left_chopstick = 1) & !(right_chopstick = 2): 0;
      TRUE : left_chopstick;
    esac;

    next(right_chopstick) := case
      (state = pickup) & (left_chopstick = 1) & (right_chopstick = 0): 2;
      (state = putdown) & (right_chopstick = 2): 0;
      TRUE : right_chopstick;
    esac;

    next(ALTRUIST) := case
      (DEADLOCK) & (ALTRUIST = ID): (ALTRUIST mod 5) + 1;
      TRUE : ALTRUIST;
    esac;

FAIRNESS  running

该代码，即使对于不了解NuSMV的人来说，也应该是不言自明的。

模型的其余部分在这里展示：

MODULE main

  VAR
    chopstick1 : 0..2;
    chopstick2 : 0..2;
    chopstick3 : 0..2;
    chopstick4 : 0..2;
    chopstick5 : 0..2;

    ph1 : process philosopher(1, chopstick1, chopstick2, ALTRUIST, DEADLOCK);
    ph2 : process philosopher(2, chopstick2, chopstick3, ALTRUIST, DEADLOCK);
    ph3 : process philosopher(3, chopstick3, chopstick4, ALTRUIST, DEADLOCK);
    ph4 : process philosopher(4, chopstick4, chopstick5, ALTRUIST, DEADLOCK);
    ph5 : process philosopher(5, chopstick5, chopstick1, ALTRUIST, DEADLOCK);

    ALTRUIST : 1..5;

  ASSIGN
    init(chopstick1) := 0;
    init(chopstick2) := 0;
    init(chopstick3) := 0;
    init(chopstick4) := 0;
    init(chopstick5) := 0;

  DEFINE
    DEADLOCK :=
      chopstick1 = 1 &
      chopstick2 = 1 &
      chopstick3 = 1 &
      chopstick4 = 1 &
      chopstick5 = 1;

    some_eating :=
      ph1.state = eat |
      ph2.state = eat |
      ph3.state = eat |
      ph4.state = eat |
      ph5.state = eat ;

    adjacent_eating :=
      (ph1.state = eat & ph2.state = eat) |
      (ph2.state = eat & ph3.state = eat) |
      (ph3.state = eat & ph4.state = eat) |
      (ph4.state = eat & ph5.state = eat) |
      (ph5.state = eat & ph1.state = eat) ;

    all_pickup :=
      ph1.state = pickup &
      ph2.state = pickup &
      ph3.state = pickup &
      ph4.state = pickup &
      ph5.state = pickup ;

    number_eating :=
      toint(ph1.state = eat) +
      toint(ph2.state = eat) +
      toint(ph3.state = eat) +
      toint(ph4.state = eat) +
      toint(ph5.state = eat) ;


-- Never two neighboring philosophers eat at the same time.
LTLSPEC G !adjacent_eating

-- No more than two philosophers can eat at the same time.
LTLSPEC G (number_eating <=2)

-- Somebody eats infinitely often.
LTLSPEC G F some_eating

-- If every philosopher holds his left fork, sooner or later somebody will get the opportunity to eat.
LTLSPEC G (all_pickup -> F some_eating)
LTLSPEC  ! ( F G all_pickup )
于 2016-07-13T21:21:52.903 回答