ABSTRAK
Perkenalan
Programmer sistem terdistribusi mengandalkan Replicated Data Types (RDT), yang menyerupai tipe data sekuensial tetapi menggabungkan strategi penyelesaian konflik untuk menjamin konvergensi saat konflik terjadi. Semantik RDT bergantung pada strategi penyelesaian konflik yang mendasarinya, tetapi ini tidak dapat disesuaikan. Selain itu, memastikan konvergensi status saja tidak cukup karena status yang dihasilkan dapat merusak invarian khusus aplikasi. Meskipun beberapa pendekatan mendukung invarian tingkat aplikasi di atas RDT yang ada , pendekatan tersebut tidak membantu membangun RDT sejak awal. Akibatnya, RDT kustom diimplementasikan menggunakan pendekatan ad hoc, yang diketahui rawan kesalahan dan menghasilkan sistem yang rapuh. Kami sebelumnya mengusulkan Explicitly Consistent Replicated Objects (ECRO) untuk mengatasi masalah ini, yang memungkinkan programmer membangun RDT kustom dengan menambah tipe data sekuensial dengan spesifikasi terdistribusi. Namun, spesifikasi tersebut memerlukan formalisasi logika orde pertama yang lengkap dari tipe data dan operasinya, yang sulit dikembangkan. Lebih jauh, kesalahan kecil dalam spesifikasi dapat mengakibatkan anomali runtime seperti divergensi status dan invarian yang rusak.
Metode
Untuk mengatasi masalah ini, kami menggabungkan model pemrograman ECRO dengan verifikasi program otomatis. Hasilnya adalah EFx, bahasa pemrograman berorientasi objek minimalis yang intinya terdiri dari sistem kontrak yang menyederhanakan pengembangan RDT. EFx tidak memerlukan spesifikasi logika orde pertama yang membosankan karena menganalisis implementasi tipe data, sehingga mencegah anomali runtime karena kesalahan dalam spesifikasi.
Hasil
Kami merekonstruksi portofolio asli ECRO di EFx untuk memvalidasi pendekatan kami. Kami secara konsisten mencapai pengurangan ukuran kode sebanyak 2x hingga 4x. Selain itu, kami menerapkan beberapa aplikasi, seperti sistem lelang RUBiS, tolok ukur SmallBank, permainan pemungutan suara terdistribusi, dan sistem reservasi maskapai penerbangan.
Kesimpulan
Evaluasi kami menunjukkan bahwa EFx menyederhanakan pengembangan RDT.
