Cara Menguji Struktur Data Konkuren dengan Benar

 (matklad.github.io)
2 poin oleh GN⁺ 2024-07-07 | 1 komentar | Bagikan ke WhatsApp
  • Menggunakan counter konkuren Rust yang rusak sebagai contoh, artikel ini mengungkap masalah yang terlewat oleh uji beban thread biasa lewat kontrol urutan eksekusi yang dapat direproduksi dan diminimalkan
  • Pembungkus AtomicU32 untuk pengujian menyisipkan pause(), dan managed thread berhenti sebelum dan sesudah operasi atomik lalu dilanjutkan lagi sesuai urutan yang dipilih pengujian
  • Pengujian sederhana dapat membuat kegagalan seperti 9598 alih-alih nilai yang diharapkan 10000 ketika 100 thread masing-masing menaikkan nilai 100 kali, tetapi karena bergantung pada timing, kasus ini sulit direproduksi, di-debug, dan diperkecil
  • Uji properti berbasis arbtest dapat mereproduksi interleaving yang sama dengan seed yang sama, dan meminimalkan kasus gagal hingga menjadi 0: increment, 1: increment, 0: unpause, 1: unpause
  • Jika struktur yang sama diperluas dengan exhaustigen, semua interleaving hingga maksimum 5 kali increment dapat didaftarkan, dan setelah diperbaiki dengan fetch_add, 81133 interleaving lolos

Counter konkuren yang tidak atomik

  • Contohnya memakai AtomicU32 dari Rust, tetapi increment() melakukan load lalu store(value + 1), sehingga operasi increment itu sendiri tidak atomik
  • Struktur Counter sederhana
    • value: AtomicU32
    • increment() membaca nilai dengan SeqCst, menambahkan 1 ke nilai yang dibaca, lalu menyimpannya kembali
    • get() membaca nilai saat ini dengan SeqCst
  • Dua thread dapat membaca nilai yang sama lalu menyimpan hasil increment yang sama, sehingga ada update yang hilang

Mengapa pengujian thread biasa tidak cukup

  • Verifikasi paling sederhana adalah membuat beberapa thread berulang kali menaikkan counter yang sama lalu memeriksa nilai akhirnya
    • thread_count = 100
    • increment_count = 100
    • nilai yang diharapkan adalah 10000
  • Contoh eksekusi gagal dengan left: 9598, right: 10000
  • Pendekatan ini sangat bergantung pada timing penjadwalan
    • sulit mereproduksi kegagalan yang sama secara deterministik
    • sulit di-debug
    • jika jumlah thread atau jumlah increment dikurangi, pengujian bisa lolos karena kebetulan, sehingga sulit meminimalkan kasus gagal

Menangani interleaving dengan pengujian berbasis properti

  • Pengujian berbasis properti (PBT) cocok dengan pengujian state machine
    • mudah menghasilkan input acak
    • dapat menetapkan properti bahwa hasil eksekusi konkuren harus sama dengan model eksekusi sekuensial
    • juga cocok dengan kebutuhan untuk meminimalkan input yang gagal
  • Tantangannya adalah sulit menjalankan thread OS sungguhan selangkah demi selangkah pada waktu yang diinginkan
  • Solusinya adalah struktur yang pada setiap iterasi memilih thread acak untuk dijalankan satu langkah
    • harus bisa menyisipkan thread lain di antara load dan store milik satu thread
    • untuk itu dibangun API managed thread yang bisa mengendalikan thread secara langsung

AtomicU32 untuk pengujian dan penyisipan pause

  • Pada build pengujian, digunakan managed_thread::AtomicU32 buatan sendiri alih-alih std::sync::atomic::AtomicU32
    • #[cfg(test)] use managed_thread::AtomicU32
    • #[cfg(not(test))] use std::sync::atomic::AtomicU32
  • Pembungkus AtomicU32 memanggil pause() sebelum dan sesudah load() maupun store()
    • load: pause() → load sebenarnya → pause()
    • store: pause() → store sebenarnya → pause()
  • Berkat titik sisip ini, pengujian dapat menghentikan dan melanjutkan thread di sekitar operasi atomik sambil mengendalikan urutan eksekusi

Bentuk API managed thread

  • Pengujian membuat dua managed thread di dalam std::thread::scope
    • karena memakai scoped thread, data lokal di stack bisa dipinjam
    • referensi ke counter diteruskan sebagai state, misalnya spawn(scope, &counter)
  • Managed thread tidak langsung menjalankan fungsi main tertentu sejak awal, melainkan mengeksekusi closure yang dikirim thread pengendali lewat submit()
    • t.submit(|c| c.increment())
    • thread mengeksekusi closure terhadap state T miliknya
  • Selama masih ada entropi, loop pengujian memilih aksi acak untuk setiap thread
    • jika thread sedang berhenti, panggil unpause()
    • jika tidak berhenti, jalankan increment() lewat submit()
    • model sekuensial counter_model juga dinaikkan dengan jumlah yang sama
  • Pada akhirnya, semua thread di-join() dan counter_model dibandingkan dengan counter.get() yang sebenarnya

Implementasi pause dan unpause

  • Agar API Counter yang diuji tidak perlu diubah, pause() mencari konteks managed thread saat ini melalui thread_local!
    • konteks dibagikan sebagai Arc<SharedContext>
    • SharedContext memiliki Mutex<State> dan Condvar
  • Status dibagi menjadi Ready, Running, dan Paused
    • Ready: sedang menunggu closure berikutnya
    • Running: managed thread sedang berjalan
    • Paused: berhenti di titik pause()
  • Saat managed thread mencapai pause(), status diubah dari Running menjadi Paused dan thread pengendali diberi tahu lewat condition variable
  • unpause() mengubah status dari Paused menjadi Running, membangunkan managed thread, lalu menunggu lagi sampai statusnya bukan Running
    • ini mencegah thread pengendali dan managed thread terus berjalan bersamaan
    • pada waktu mana pun hanya salah satu yang berjalan, sehingga nondeterminisme berkurang

Reproduksi dan minimisasi kegagalan

  • Eksekusi arbtest menemukan kegagalan pada counter yang rusak
    • contoh kegagalan: nilai model 4, nilai aktual 3
    • seed kegagalan: 0x4fd7ddff00000020
  • Dengan seed yang sama, interleaving yang sama bisa didapat kembali, sehingga reproduksi kegagalan menjadi mudah
  • Dengan .minimize(), kasus gagal diperkecil menjadi eksekusi yang lebih singkat
    • seed akhir yang minimal adalah 0x9c2a13a600000001
    • trace minimal memiliki empat langkah
      • 0: increment
      • 1: increment
      • 0: unpause
      • 1: unpause
  • Pada kasus minimal ini, nilai yang diharapkan adalah 2 tetapi nilai aktual 1, sehingga cacat pada increment berbasis load/store terlihat jelas

Diperluas dengan enumerasi semua interleaving

  • Struktur yang sama bisa diubah dari interleaving acak menjadi pendekatan berbasis enumerasi
  • Dengan exhaustigen, dibuat pengujian yang menjelajahi semua interleaving hingga maksimum 5 kali increment
    • pengujian disusun agar menghindari iterasi dummy, dan selalu melakukan unpause pada thread atau mengirim increment
  • Implementasi yang rusak menemukan bug yang sama
    • contoh kegagalan: left: 2, right: 1
  • Setelah Counter::increment() diperbaiki menjadi fetch_add(1, SeqCst), pengujian lolos
    • pembungkus AtomicU32 juga ditambahkan pause() sebelum dan sesudah fetch_add()
    • hasil eksekusi: all 81133 interleavings are fine!
    • waktu eksekusi: real 8.65s, CPU 8.16s, RSS 63.91mb

Perluasan ke model memori lemah dan model checking

  • Implementasi AtomicU32 mainan saat ini mendelegasikan ke atomic sungguhan
  • Ide pengembangannya adalah setiap atomic menyimpan himpunan nilai yang pernah ditulis, lalu saat membaca mengembalikan nilai acak yang konsisten dengan model memori lemah
  • Penjelajahan interleaving juga bisa dibuat lebih cerdas daripada sekadar acak
    • dengan pendekatan model checking, kita bisa memastikan apakah semua interleaving yang bermakna berbeda sudah dipertimbangkan
    • seperti pendekatan Generate All The Things, semua interleaving dalam cakupan kecil dapat didaftarkan

Mengapa minimisasi bisa dilakukan tanpa shrinking

  • arbtest yang digunakan tampak seperti antarmuka PRNG yang familier, tetapi memakai PRNG hingga
    • jika nilai acak terus diminta, pada suatu titik ia akan mengembalikan Err(OutOfEntropy)
    • karena itu di kode pengujian muncul ? dan while !rng.is_empty()
  • Saat pengujian menghabiskan entropi, eksekusi berakhir lebih cepat, sehingga jika entropi yang tersedia dikurangi, eksekusi pengujian juga menjadi lebih pendek
  • Implementasi internalnya secara konseptual mirip &mut &[u8]
    • setiap kali angka acak diminta, irisan byte menjadi lebih pendek
    • makin pendek irisan awalnya, makin sederhana pengujiannya
  • Berkat pendekatan ini, kasus gagal bisa dipersingkat tanpa perlu mengimplementasikan logika shrinking terpisah secara manual
  • Kode sumber contohnya ada di properly-concurrent

Bacaan terkait

1 komentar

 
GN⁺ 2024-07-07
Komentar Hacker News

  • Di Rust, ada yang sedang membuat pustaka bernama Temper dengan pendekatan serupa: https://github.com/reitzensteinm/temper/tree/main
    Namun untuk memodelkan implikasi aneh yang ditimbulkan oleh keseluruhan model memori Rust, perlu melangkah jauh lebih dalam, sehingga dibutuhkan semacam buku besar yang melacak penulisan mana yang telah diketahui oleh tiap thread. Bergantung pada urutan memori atomik, fence baca/tulis, dan sebagainya, bisa muncul jaminan seperti: jika penulisan X diketahui, maka penulisan Y juga harus diketahui
    Saya rasa ini termasuk kumpulan kasus uji model memori C++/Rust yang paling banyak; hampir semua yang bisa ditemukan dari buku, standar C++, Stack Overflow, blog, dan lain-lain sudah dikumpulkan. Misalnya, berkas untuk Rust Atomics and Locks karya Mara Bos ada di sini: https://github.com/reitzensteinm/temper/blob/main/memlog/tes...
    Loom yang disebutkan dalam tulisan tersebut serupa, tetapi merupakan pustaka yang jauh lebih matang, dan memungkinkan pengujian menyeluruh terhadap komponen tingkat lebih tinggi seperti mutex atau queue: https://github.com/tokio-rs/loom Namun model memorinya sendiri tidak dimodelkan serinci Temper, dan saya sempat berpikir untuk memindahkan kasus-kasus uji tersebut ke Loom
    Saya terinspirasi oleh presentasi Will Wilson tentang pengujian FoundationDB, dan sekarang ia sedang membuat solusi berbasis hypervisor di Antithesis untuk melakukan pengujian semacam ini pada container Docker arbitrer: https://www.youtube.com/watch?v=4fFDFbi3toc, https://antithesis.com/
    Saya sangat yakin area ini akan tumbuh jauh lebih besar dalam 10 tahun ke depan. WebAssembly berada di titik yang pas: cukup lengkap untuk mengompilasi perangkat lunak arbitrer, tetapi cukup sederhana sehingga membangun sesuatu seperti Antithesis tidak perlu menjadi proyek 5 tahun bagi tim elite yang sudah pernah merilis database

  • Saya mengimplementasikan snapshot atomik memori bersama di Rust, dan juga menangani pengujian otomatis seserius mungkin: https://github.com/kaymanb/todc/tree/main/todc-mem
    Awalnya saya memakai Loom yang disebut dalam tulisan, tetapi kemudian beralih ke shuttle: https://github.com/tokio-rs/loom, https://github.com/awslabs/shuttle
    shuttle memakai pendekatan teracak alih-alih exhaustive search seperti Loom, tetapi scheduler-nya tetap memberikan jaminan probabilistik untuk menemukan bug. Dari pengalaman saya, shuttle lebih cepat dan dapat diskalakan hingga skenario pengujian yang lebih kompleks
    Mirip dengan pendekatan dalam tulisan, jika jadwal tertentu menyebabkan pengujian gagal, seed acaknya bisa disimpan. Kemampuan mereproduksi pengujian yang gagal dengan cepat sangat penting, dan memungkinkan kita menulis test case eksplisit untuk bug yang sebelumnya ditemukan dan sudah diperbaiki: https://github.com/kaymanb/todc/blob/0e2874a70ec8beed8fae773...

  • Di sisi Kotlin/Java, Lincheck dari JetBrains adalah pustaka yang bagus untuk pekerjaan seperti ini: https://github.com/JetBrains/lincheck
    Saya terutama suka karena sifatnya deklaratif dan caranya menampilkan hasil linearizability

  • Saya penasaran apakah ada pustaka seperti Loom untuk C++. Ada beberapa struktur data lock-free yang ingin saya uji

  • Jika saya memahaminya dengan benar, pendekatan ini punya keterbatasan terkait jaminan kemajuan maju yang lemah.
    Perhitungan di artikel memang tidak sepenuhnya sepele, tetapi di perangkat keras nyata dan scheduler nyata, kita bisa membayangkan loop cmpxchg yang kemungkinannya berhenti di CPU tertentu sangat kecil. Jika jumlah CPU adalah n, dalam kasus terburuk peluang untuk maju adalah 1/n, tetapi dalam metode pengujian ini menjadi 1/t^p. Di sini t adalah jumlah task, yang bisa jauh lebih besar daripada jumlah CPU, dan p adalah jumlah jeda di dalam body loop tersebut, yang dengan mudah bisa 3 atau lebih. Ini sudah cukup untuk membuat algoritma yang sebenarnya bekerja terlihat rusak.
    Sebaliknya, bahkan jika kita ingin menangkap kemajuan maju yang lemah sebagai bug sehingga menuntut kemajuan maju yang kuat, metode ini tampaknya juga tidak menyediakan alat yang berguna.
    Meski begitu, untuk banyak masalah konkurensi metode ini jelas berguna.

    • 1/t^p rasanya tidak tepat; saya melihatnya hanya sebagai 1/t. Pada akhirnya, setelah waktu t berlalu, pasti ada satu task yang maju, dan jika ada t task, peluang bahwa task yang maju itu adalah task saya adalah 1/t.
      Kebingungan utamanya sepertinya ada pada anggapan bahwa jika berhenti, itu pasti berarti kalah di CAS, padahal tidak begitu.

  • Mengenai bagian “sejujurnya, ada sedikit pengetahuan sebelumnya di sini. Kecuali melakukan sesuatu yang sangat terkutuk dengan assembly inline, tampaknya kita tidak bisa menghindari pembuatan thread sungguhan. Jika sesuatu memanggil fungsi pause() dan kita ingin membuatnya berhenti sampai ada instruksi berikutnya, hal itu harus terjadi di dalam thread yang mempertahankan stack terpisah dari stack pengujian”, saya penasaran apakah tidak bisa memakai semacam runtime asinkron.
    Ini terlihat seperti mencapai multitasking kooperatif dengan menginstrumentasi operasi atomik. Mungkin saya perlu minum lebih banyak kopi, tetapi tampaknya lebih sederhana jika dilakukan tanpa thread.

    • Memakai async memang akan nyaman, tetapi persyaratan lainnya adalah kita tidak ingin mengubah API yang terlihat dari luar pada perangkat lunak yang diuji. Async itu “menular”, jadi untuk API sinkron harus memakai implementasi sinkron.

  • Salah satu kekurangan pendekatan ini adalah kode yang diuji sendiri harus dimodifikasi agar sesuai dengan kode pengujian.
    Rasanya hal yang sama bisa dilakukan dengan menjalankan dua thread, lalu memakai ptrace untuk single-step dan menyisipkan eksekusi instruksi secara “acak”. Mirip mode chaos di rr.
    Namun karena beberapa instruksi mungkin tidak atomik, jika memang memungkinkan tanpa emulasi, sepertinya diperlukan cara untuk melakukan single-step pada satuan “mikrokode atomik”.

    • Terdengar seperti hypervisor milik Antithesis.

  • Untuk memakai Loom, sepertinya diperlukan kompilasi kondisional, dan itu mungkin oke saat menguji satu library, tetapi cukup invasif.
    #[cfg(loom)]
    pub(crate) use loom::sync::atomic::AtomicUsize;
    #[cfg(not(loom))]
    pub(crate) use std::sync::atomic::AtomicUsize;
    Saya penasaran apakah ada bahasa yang memungkinkan penggunaan scheduler sendiri dengan lebih baik.

  • Jika ingin benar-benar menyeluruh, sepertinya pengujian bisa dijalankan dengan ptrace, lalu thread dijalankan secara single-step untuk membuat interleaving berbeda di tingkat instruksi. Saya penasaran apakah ada yang pernah melihat pendekatan seperti itu dalam praktik.
    Jika kode tidak bisa diinstrumentasi seperti di sini, apakah ada alternatif untuk pengujian black-box?

    • Saya pernah memakai pendekatan seperti itu untuk menguji handler sinyal asinkron, tetapi di kasus itu jumlah kombinasinya jauh lebih menguntungkan. Jika thread utama menjalankan n instruksi, kita hanya perlu n kali eksekusi, yaitu menjalankan 0 sampai n instruksi sebelum menyisipkan sinyal; setelah itu handler sinyal berjalan sampai selesai, lalu thread utama juga berjalan sampai selesai. Total waktunya O(n^2).
      Namun jika ada t thread yang masing-masing menjalankan n instruksi, dan semuanya bisa saling menghentikan di setiap batas, pendekatan ini sulit diterapkan untuk nilai n yang realistis. Sepertinya perlu dipersempit dengan memilih dan menyimulasikan hanya operasi yang memiliki perilaku menarik.

  • Terlihat cukup keren, jadi saya harus mencobanya. Namun ini tidak akan menangkap semua jenis kesalahan. Setiap pemanggilan pause() menciptakan sinkronisasi antar-thread, jadi bukankah sebagian masalah data race bisa tertutupi? Di Rust mungkin ini bukan masalah.