Model Konkurensi dan Kalkulus Proses

Model konkurensi dan kalkulus proses memberikan penjelasan formal tentang bagaimana proses independen dieksekusi, berkomunikasi, dan melakukan sinkronisasi.

Definition

Kalkulus proses adalah aljabar formal untuk menggambarkan sistem konkuren sebagai proses yang berkomunikasi, dengan operator untuk komposisi paralel, komunikasi, dan pilihan, serta kesetaraan yang menentukan kapan dua proses berperilaku sama.

Scope

Topik ini mencakup model aljabar komputasi konkuren: CSP Hoare dan CCS Milner, pi-kalkulus untuk proses bergerak yang topologi komunikasinya berubah, dan model aktor dari pengiriman pesan asinkron. Ini membahas primitif komunikasi dan sinkronisasi, kesetaraan perilaku seperti bisimulasi, dan kontras antara konkurensi memori bersama dan pengiriman pesan.

Core questions

• Bagaimana proses komunikasi konkuren dapat dijelaskan secara aljabar?
• Kapan dua proses konkuren secara perilaku setara?
• Bagaimana perbandingan pengiriman pesan dengan konkurensi memori bersama?
• Bagaimana struktur komunikasi dinamis dimodelkan, seperti dalam pi-kalkulus?

Key theories

Proses Sekuensial Berkomunikasi (CSP)

CSP Hoare memodelkan konkurensi melalui proses yang melakukan sinkronisasi pada peristiwa komunikasi bersama, menyediakan dasar untuk bahasa pengiriman pesan dan teori penyempurnaan proses.

CCS dan bisimulasi

Kalkulus Sistem Berkomunikasi Milner memberikan aljabar proses dengan gagasan yang tepat tentang kesetaraan perilaku, bisimulasi, untuk penalaran tentang kapan proses dapat dipertukarkan.

Pi-kalkulus

Milner, Parrow, dan Walker memperluas kalkulus proses ke mobilitas, memungkinkan saluran komunikasi itu sendiri dilewatkan sebagai pesan sehingga struktur koneksi berkembang secara dinamis.

Clinical relevance

Kalkulus proses dan model aktor mendasari desain bahasa dan kerangka kerja konkuren dan terdistribusi yang dibangun di atas pengiriman pesan, dan keduanya menyediakan alat formal untuk menentukan dan memverifikasi protokol. Bisimulasi dan penyempurnaan memberikan kriteria yang tepat untuk perilaku konkuren yang benar.

History

Teori konkurensi matang pada akhir 1970-an dengan CSP Hoare dan CCS Milner, sementara model aktor Hewitt (1973) menawarkan alternatif pengiriman pesan asinkron. Pi-kalkulus pada tahun 1992 menangkap mobilitas proses. Kalkulus ini memengaruhi bahasa pengiriman pesan dan pustaka konkurensi serta tetap menjadi fondasi untuk verifikasi protokol.

Debates

Memori bersama versus pengiriman pesan

Pertanyaan desain fundamental adalah apakah konkurensi harus diatur di sekitar keadaan mutabel bersama dengan sinkronisasi atau di sekitar proses terisolasi yang bertukar pesan, dengan kalkulus proses dan model aktor yang mendukung yang terakhir.

Key figures

• C. A. R. Hoare
• Robin Milner
• Carl Hewitt
• Joachim Parrow
• David Walker

Seminal works

• hoare1978
• milner1989
• milner1992
• hewitt1973

Frequently asked questions

Apa itu bisimulasi?

Bisimulasi adalah kesetaraan pada proses yang berlaku ketika masing-masing dapat mencocokkan langkah-langkah yang dapat diamati satu sama lain tanpa batas, memformalkan gagasan bahwa dua proses konkuren menunjukkan perilaku yang sama.

Apa yang ditambahkan pi-kalkulus dibandingkan kalkulus sebelumnya?

Pi-kalkulus memodelkan mobilitas dengan memungkinkan saluran komunikasi dikirim sebagai pesan, sehingga topologi siapa yang dapat berbicara dengan siapa dapat berubah selama eksekusi, menangkap sistem yang dinamis dan dapat dikonfigurasi ulang.