VERIFIKASI ALGORITMA DISTRIBUTED MUTUAL EXCLUSION DENGAN PROMELA/SPIN

Beberapa sumber daya (resource) pada sistem terdistribusi, hanya boleh diakses
secara mutually exclusive untuk mencapai hasil yang diinginkan bersama. Akses inilah
yang menyebabkan terjadinya masalah mutual exclusion; akses dimana sumber daya
tersebut tidak dapat dieksekusi sekaligus oleh proses yang banyak dalam waktu yang
bersamaan. Jadi proses-proses kongkuren (concurrent processes) yang kondisinya pada
saat bersamaan melakukan share terhadap sumber daya membutuhkan algoritma mutual
exclusion untuk menjamin hanya satu proses yang mengakses sumber daya pada satu
waktu tertentu.
Beberapa algoritma terdistribusi (distributed algorithms) dapat menyelesaikan
masalah ini dengan prinsip kerja yang juga berbeda. Dalam bahasan ini akan membahas
bagaimana algoritma tersebut dibuktikan secara matematis, dan juga dengan verifikasi
menggunakan tools SPIN (Simple Promela Interpreter) yang dimodelkan menggunakan
bahasa PROMELA (Protocol/Process Meta Language) yang menyerupai bahasa C.