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

あなたのコードの落とし穴は、隣人の誰かがすでに食べようとしている場合、すべての哲学者が食べることを控えることです。

すべての哲学者が利己的で、できるだけ多くのフォークを単純につかむと、行き詰まりの状況に陥る可能性があることに気付いた後で、この方法でコードを設計した可能性があります。

適切な解決策は、両極端の中にあります。各哲学者の食べるという強いコミットメントを、デッドロックを回避するのに十分なだけ緩和する必要がありますが、飢餓に陥るほどではありません。

飢餓に陥ることなくデッドロックを回避するための可能なアプローチは、利他的哲学者の概念を導入することです。これは、デッドロック状況があるために誰も食べることができないことに気付いたときに、保持しているフォークをドロップする哲学者です。

デッドロックを回避するには、利他的な哲学者が1 人 いるだけで十分です。したがって、他のすべての哲学者は貪欲であり続け、できるだけ多くのフォークをつかもうとすることができます。

ただし、処刑中に利他的哲学者を変更しないと、その男が餓死する可能性があります。したがって、解決策は、利他的な哲学者を無限に頻繁に変更することです。公正な戦略は、1 人の哲学者が行き詰まりの状況で利他的に行動するたびに、ラウンド ロビン方式で変更することです。そうすれば、哲学者は罰せられず、スケジューラーがすべての哲学者に無限に頻繁に実行する機会を与えるという公平な条件の下で飢えている哲学者がいないことを実際に検証できます。

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 に答える