Titik Koma yang Bocor
Author
Venue
Prosiding ACM tentang Bahasa Pemrograman 2021
Abstract
Logika dan semantik program menceritakan kisah yang menyenangkan tentang komposisi berurutan: saat menjalankan (S1; S2), kita terlebih dahulu menjalankan S1 lalu S2. Namun, untuk meningkatkan kinerja, prosesor menjalankan instruksi secara acak, dan kompiler bahkan lebih drastis dalam mengatur ulang urutan program. Secara desain, sistem single-threaded tidak dapat mengamati pengaturan ulang ini; namun, sistem multi-threaded dapat melakukannya, sehingga kisah tersebut menjadi jauh kurang menyenangkan. Upaya formal untuk memahami kekacauan yang dihasilkan dikenal sebagai "model memori yang dilonggarkan." Model-model sebelumnya gagal menangani komposisi berurutan secara langsung, atau terlalu membatasi prosesor dan kompiler, atau memperbolehkan perilaku yang tidak masuk akal yang tidak dapat diamati dalam praktik. Untuk mendukung komposisi berurutan sambil menargetkan perangkat keras modern, kami memperkaya pendekatan berbasis peristiwa standar dengan prasyarat dan keluarga transformator predikat. Saat menghitung makna (S1;S2), transformator predikat yang diterapkan pada prasyarat suatu peristiwa e dari S2 dipilih berdasarkan himpunan peristiwa dalam S1 yang menjadi dasar e. Kami menerapkan pendekatan ini pada dua model memori yang ada.
