communicating sequential processes

Angol

Főnév

communicating sequential processes (tsz. communicating sequential processeses)

1. (informatika) A Communicating Sequential Processes (CSP) egy formális modell, amelyet a párhuzamos (konkurens) rendszerek viselkedésének leírására és elemzésére fejlesztett ki Sir Tony Hoare 1978-ban. A CSP segítségével matematikailag pontosan modellezhetjük a több független folyamatot, amelyek üzenetküldéssel kommunikálnak.

---

📌 Alapgondolat

A CSP azt az elvet követi, hogy:

Egy rendszer több független folyamatból áll, amelyek csak üzenetek révén kommunikálnak, és nem osztanak meg közös memóriát.

Ez radikálisan eltér a hagyományos, megosztott memóriás szinkronizációs modellektől (mint például mutexek, szemináriumok), és inkább a hálózaton keresztüli kommunikációhoz vagy aktormodellekhez hasonlít.

---

🧠 Miért hasznos?

• Konkurens rendszerek tervezése és analízise (pl. párhuzamos programok, hálózati protokollok)
• Helyesség bizonyítása (pl. halhatatlanság, holtpontmentesség, determinisztikus viselkedés)
• Model checking eszközök alapja (pl. FDR – Failures-Divergence Refinement)
• Hatással volt a Go, Rust, Erlang és Occam nyelvek tervezésére

---

🔩 Fő fogalmak

1. Folyamatok (Processes)

• Egy CSP-folyamat egy önálló egység, amely eseményeket hajt végre
• Pl. P = a → b → STOP jelentése: hajtsa végre az a eseményt, majd a b-t, majd álljon le

2. Események (Events)

• Absztrakt szinkronizációs jelek, mint read, write, send, receive
• Események csak akkor történnek meg, ha mindkét fél készen áll (szinkron kommunikáció)

3. Kommunikáció

• Egy csatornán keresztül történik
• A c!v egy érték (v) küldése a c csatornán
• A c?x egy érték fogadása, amit változóba (x) ment

---

🔧 Operátorok és szintaxis

Prefixálás

a → P

→ hajtsa végre az a eseményt, majd folytassa a P folyamattal

---

Párhuzamos végrehajtás

P || Q

→ P és Q egyszerre futnak, és szinkronizálódnak közös eseményekre

---

Kizárólagos választás

a → P □ b → Q

→ választható az a vagy b, attól függően, melyik történik meg előbb

---

Szinkronizált kommunikáció

Ha P = c!5 → STOP és Q = c?x → STOP, akkor P || Q → a c.5 esemény csak akkor történik meg, ha mindkét folyamat készen áll

---

Rekurzió

X = a → X

→ végtelenül ismétli az a eseményt

---

🧪 Egyszerű példa

Képzeljük el, hogy van egy producer és egy consumer, akik egy értéket cserélnek:

Producer = produce!x → STOP
Consumer = produce?y → STOP
System = Producer || Consumer

• A produce egy csatorna
• A System csak akkor haladhat tovább, ha a producer küld, és a consumer fogad – ez a CSP szinkron kommunikáció kulcsa

---

🧰 Elméleti háttér

A CSP formálisan a következőkkel dolgozik:

• Traces: események sorozata (pl. [a, b, c])
• Failures: (trace, események, amelyeket a folyamat elutasíthat egy adott ponton)
• Divergence: végtelen belső aktivitás lehetősége (pl. holtpontmentesség vizsgálatához)

Ez lehetővé teszi a folyamatok viselkedésének matematikai összehasonlítását, például: P ⊑ Q (P refine-olja Q-t)

---

🔐 Példák használatra

1. Beágyazott rendszerek

• Az Occam nyelv, amelyet az Inmos Transputer gépekhez terveztek, teljes egészében CSP-re épül

2. Model Checking

• Az FDR (Failures-Divergences Refinement) nevű eszköz segítségével automatizálható a CSP modellek helyességellenőrzése

3. Programozási nyelvek

• Go:
  • goroutine + channel szinkronizáció = CSP ihlette
  • Pl.: x := <-ch és ch <- x
• Rust:
  • crossbeam és tokio csatornák CSP-szerű viselkedést valósítanak meg
• Erlang:
  • Üzenetküldés aktorok között: bár nem szinkron, a gondolat hasonló

---

🏁 Példa CSP viselkedésre

Clock = tick → Clock
Sensor = measure → send!data → Sensor
Controller = send?d → process(d) → Controller
System = Sensor || Controller

• A Sensor periodikusan mér és küld adatot
• A Controller csak akkor tud feldolgozni, ha kap adatot
• A System a két folyamat párhuzamos együttműködését modellezi

---

⚠️ CSP vs Actor Model

Tulajdonság	CSP	Actor Model
Kommunikáció típusa	Szinkron (két fél egyszerre)	Aszinkron (üzenetküldés postán)
Memóriamegosztás	Nincs	Minden aktor saját állapottal bír
Tipikus nyelv	Occam, Go	Erlang, Akka

---

📚 Források és eszközök

• Könyv: Communicating Sequential Processes (Tony Hoare, 1985)
• Model checking eszköz: FDR4 – Oxford által fejlesztve
• Következő generációs nyelvek: Go, Rust, Pony, Clojure’s core.async

---

🧠 Összefoglalás

A CSP egy elegáns, formális eszköz arra, hogy párhuzamos rendszereket írjunk le, elemezzünk, és biztosítsuk azok helyességét. A kulcs az, hogy a folyamatok nem osztanak meg memóriát, hanem szinkron üzenetküldéssel kommunikálnak. Ezáltal elkerülhetők a versenyhelyzetek és holtpontok — ha jól tervezzük meg a rendszert. A modern nyelvek számos eleme (mint a Go csatornák) közvetlenül ebből az elméletből ered.

További információk

• communicating sequential processes - Szótár.net (en-hu)
• communicating sequential processes - Sztaki (en-hu)
• communicating sequential processes - Merriam–Webster
• communicating sequential processes - Cambridge
• communicating sequential processes - WordNet
• communicating sequential processes - Яндекс (en-ru)
• communicating sequential processes - Google (en-hu)
• communicating sequential processes - Wikidata
• communicating sequential processes - Wikipédia (angol)