Co oznacza „prawdziwa współbieżność”?

Często słyszę wyrażenia takie jak „semantyka prawdziwej współbieżności” i „równoważność prawdziwej współbieżności” bez żadnych odniesień. Co oznaczają te terminy i dlaczego są ważne?

Jakie są przykłady prawdziwych odpowiedników współbieżności i jaka jest ich potrzeba? Np. W jakich przypadkach mają one większe zastosowanie niż więcej standardowych równoważników (bisimulacja, równoważność śladowa itp.)?

Termin „prawdziwa współbieżność” pojawia się w teoretycznym badaniu obliczeń współbieżnych i równoległych. Jest to przeciwieństwo współbieżności przeplatania. Prawdziwa współbieżność to współbieżność, której nie można sprowadzić do przeplatania. Współbieżność jest przeplatana, jeżeli na każdym etapie obliczeń może mieć miejsce tylko jedna akcja obliczeń atomowych (np. Wymiana wiadomości między nadawcą a odbiorcą). Współbieżność jest prawdą, jeśli więcej niż jedno takie działanie atomowe ma miejsce w jednym kroku.

Najprostszym sposobem na rozróżnienie obu jest przyjrzenie się regule dla kompozycji równoległej. W ustawieniach opartych na przeplataniu wyglądałoby to mniej więcej tak:

$$\frac{P \rightarrow P'}{P|Q \rightarrow P'|Q}$$

Ta reguła wymusza, że ​​tylko jeden proces w składzie równoległym może wykonać akcję atomową. W przypadku prawdziwej współbieżności bardziej odpowiednia byłaby reguła taka jak poniżej.

$$\frac{P \rightarrow P'\quad Q \rightarrow Q'}{P|Q \rightarrow P'|Q'}$$

Ta reguła pozwala obu uczestnikom w równoległym składzie wykonywać działania atomowe.

Dlaczego ktoś interesuje się przeplataną współbieżnością, skoro teoria współbieżności jest tak naprawdę badaniem systemów, które wykonują kroki obliczeniowe równolegle? Odpowiedź brzmi: i to świetny wgląd, że w przypadku prostych form współbieżności przekazywania wiadomości, prawdziwa współbieżność i współbieżność oparta na przeplataniu nie są rozróżnialne kontekstowo. Innymi słowy, przeplatana współbieżność zachowuje się jak prawdziwa współbieżność, o ile obserwatorzy mogą to zobaczyć. Przeplatanie to dobry rozkład prawdziwej współbieżności. Ponieważ przeplatanie jest łatwiejsze w dowodach, ludzie często studiują tylko prostszą współbieżność opartą na przeplataniu (np. CCS i$\pi$-calculi). Jednak ta prostota znika w obliczeniach współbieżnych z bogatszymi formami obserwacji (np. Obliczenia czasowe): różnica między prawdziwą współbieżnością a współbieżnością przeplataną staje się zauważalna.

Standardowe równoważniki, takie jak bisimulacje i ślady, mają te same definicje dla współbieżności opartej na prawdzie i przeplataniu. Ale mogą, ale nie muszą równać różnych procesów, w zależności od rachunku różniczkowego.

Pozwólcie, że przedstawię nieformalne wyjaśnienie, dlaczego przeplatanie i prawdziwie współbieżne interakcje są nierozróżnialne w prostych obliczeniach procesowych. Ustawienie jest rachunkiem podobnym do CCS lub . Powiedzmy, że mamy program$\pi$

$$P \quad=\quad \overline{x} \ |\ \overline{y} \ |\ x.y.\overline{a} \ |\ y.\overline{b}$$ Następnie mamy następującą naprawdę równoczesną redukcję: Ten krok redukcji można uzupełnić następującymi przeplatanymi krokami: Jedyna różnica między nimi polega na tym, że pierwszy robi jeden krok, a drugi dwa. Ale proste kalkulatory nie mogą wykryć liczby kroków użytych do osiągnięcia procesu. $$\begin{eqnarray*} P &\rightarrow& y.\overline{a} \ |\ \overline{b} \end{eqnarray*}$$ $$\begin{eqnarray*} P &\rightarrow & \overline{x} \ |\ x.y.\overline{a} \ |\ \overline{b} \\ &\rightarrow & y.\overline{a} \ |\ \overline{b} \end{eqnarray*}$$

Jednocześnie ma następującą drugą przeplecioną sekwencję redukcji: Ale jest to również sekwencja redukcji w naprawdę współbieżnych ustawieniach, o ile prawdziwa współbieżność nie jest wymuszona (tj. wykonania z przeplotem są dozwolone, nawet jeśli istnieje możliwość więcej niż jednej interakcji na raz).$P$

$$\begin{eqnarray*} P &\rightarrow & \overline{y} \ |\ y.\overline{a} \ |\ y.\overline{b} \\ &\rightarrow & \overline{a} \ |\ y.\overline{b} \end{eqnarray*}$$

Prawdę mówiąc, sam szukałem odpowiedzi w Google. Jaka jest tutaj semantyka? Przypisujemy znaczenie „system przejściowy” opisowi „algebra procesu”; tzn. znaczenie to system przejściowy, który jest generowany z początkowego opisu systemu przy użyciu zdefiniowanych reguł SOS. Tak więc, stosując semantykę przeplatania, tracimy całą współbieżną strukturę w uzyskanym układzie przejściowym.

Inną odpowiedzią może być to, że nie jest to „zauważalna różnica”, ale różnica w „obserwowalności”. Stosując semantykę przeplatania, możemy obserwować tylko przebiegi liniowe; natomiast stosując prawdziwą współbieżność możemy zaobserwować „równoczesne przebiegi” (por. W.Reisig'13 książka sieci Petriego).

Mimo to mam wątpliwości co do tego, co powiedziałem powyżej, i byłoby interesujące usłyszeć głębsze spostrzeżenia. Tj. Przy użyciu zegarów wektorowych Lamporta ile teorii względności można przenieść na teorię współbieżności.