วิธีทดสอบโครงสร้างข้อมูลแบบ concurrent อย่างถูกต้อง

 (matklad.github.io)
2 คะแนน โดย GN⁺ 2024-07-07 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ใช้ตัวอย่าง counter แบบ concurrent ใน Rust ที่มีข้อบกพร่อง เพื่อเผยปัญหาที่การทดสอบโหลดด้วย thread ทั่วไปมองข้าม ด้วย การควบคุมลำดับการรันที่ทำซ้ำได้และย่อให้เล็กที่สุดได้
  • wrapper AtomicU32 สำหรับทดสอบจะแทรก pause() และ managed thread จะหยุดก่อนและหลังการดำเนินการแบบ atomic แล้วจึงรันต่อในลำดับที่การทดสอบเลือก
  • การทดสอบแบบง่ายอาจสร้างความล้มเหลวได้ เช่นให้ thread 100 ตัวเพิ่มค่าคนละ 100 ครั้ง แต่ได้ 9598 แทนค่าที่คาดไว้ 10000 ทว่าขึ้นกับ timing จึงทำซ้ำ ดีบัก และย่อกรณีได้ยาก
  • การทดสอบเชิงคุณสมบัติที่ใช้ arbtest สามารถทำซ้ำ interleaving เดิมด้วย seed เดิม และ ย่อ กรณีล้มเหลวลงเหลือ 0: increment, 1: increment, 0: unpause, 1: unpause
  • เมื่อขยายโครงสร้างเดียวกันด้วย exhaustigen จะไล่แจง interleaving ทั้งหมดได้จนถึงการเพิ่มค่าสูงสุด 5 ครั้ง และหลังแก้เป็น fetch_add แล้ว interleaving 81133 แบบผ่านทั้งหมด

Counter แบบ concurrent ที่ไม่เป็น atomic

  • ตัวอย่างใช้ AtomicU32 ของ Rust แต่ increment() ทำ load แล้วตามด้วย store(value + 1) ดังนั้น การเพิ่มค่าเองไม่ได้เป็น atomic
  • โครงสร้าง Counter เรียบง่าย
    • value: AtomicU32
    • increment() อ่านค่าด้วย SeqCst บวก 1 กับค่าที่อ่านได้ แล้วเขียนกลับไป
    • get() อ่านค่าปัจจุบันด้วย SeqCst
  • หากสอง thread อ่านค่าเดียวกันแล้วเขียนผลลัพธ์หลังเพิ่มค่าเดียวกันกลับไป การอัปเดตหนึ่งครั้งอาจหายไป

ทำไมการทดสอบด้วย thread ทั่วไปจึงไม่พอ

  • วิธีตรวจสอบที่ง่ายที่สุดคือให้หลาย thread เพิ่มค่า counter เดียวกันซ้ำ ๆ แล้วตรวจค่าท้ายสุด
    • thread_count = 100
    • increment_count = 100
    • ค่าที่คาดไว้คือ 10000
  • ตัวอย่างการรันล้มเหลวด้วย left: 9598, right: 10000
  • วิธีนี้พึ่งพา timing ของ scheduling อย่างมาก
    • ทำซ้ำความล้มเหลวเดิมแบบแน่นอนได้ยาก
    • ดีบักได้ยาก
    • หากลดจำนวน thread หรือจำนวนครั้งที่เพิ่มค่า อาจผ่านได้เพราะโชคดี จึงย่อกรณีล้มเหลวให้เล็กที่สุดได้ยาก

จัดการ interleaving ด้วยการทดสอบเชิงคุณสมบัติ

  • การทดสอบเชิงคุณสมบัติ (PBT) เข้ากันได้ดีกับการทดสอบ state machine
    • สร้างอินพุตแบบสุ่มได้ง่าย
    • ตั้งคุณสมบัติได้ว่าผลลัพธ์ของการรันแบบ concurrent ต้องเหมือนกับโมเดลที่รันแบบลำดับ
    • สอดคล้องกับความต้องการย่ออินพุตที่ล้มเหลวให้เล็กที่สุด
  • จุดยากคือการสั่งให้ OS thread จริงเดินหน้าไปทีละขั้น ณ จุดที่ต้องการทำได้ยาก
  • ทางแก้คือโครงสร้างที่ในแต่ละรอบเลือก thread แบบสุ่มมาหนึ่งตัวแล้วให้เดินหน้าไปหนึ่งขั้น
    • ต้องสามารถแทรก thread อื่นเข้ามาระหว่าง load กับ store ของ thread หนึ่งได้
    • เพื่อสิ่งนี้ จึงสร้าง API managed thread ที่ควบคุม thread ได้โดยตรง

AtomicU32 สำหรับทดสอบและการแทรก pause

  • ใน build สำหรับทดสอบ จะใช้ managed_thread::AtomicU32 ที่ทำเอง แทน std::sync::atomic::AtomicU32
    • #[cfg(test)] use managed_thread::AtomicU32
    • #[cfg(not(test))] use std::sync::atomic::AtomicU32
  • wrapper AtomicU32 เรียก pause() ก่อนและหลัง load() กับ store()
    • load: pause() → load จริง → pause()
    • store: pause() → store จริง → pause()
  • จุดที่แทรกนี้ทำให้การทดสอบหยุดและปล่อย thread ให้รันต่อรอบ ๆ การดำเนินการแบบ atomic ได้ พร้อมควบคุม ลำดับการรัน

รูปแบบของ managed thread API

  • การทดสอบสร้าง managed thread สองตัวภายใน std::thread::scope
    • เพราะใช้ scoped thread จึงยืมข้อมูลใน stack frame ได้
    • ส่ง reference ของ counter เป็นสถานะ เช่น spawn(scope, &counter)
  • managed thread ไม่ได้เริ่มด้วยการรันฟังก์ชัน main เฉพาะตั้งแต่ต้น แต่รัน closure ที่ thread ควบคุมส่งมาด้วย submit()
    • t.submit(|c| c.increment())
    • thread จะรัน closure กับสถานะ T ของตัวเอง
  • loop ของการทดสอบจะสุ่มการกระทำกับแต่ละ thread ขณะยังมี entropy เหลืออยู่
    • ถ้า thread หยุดอยู่ ให้ unpause()
    • ถ้าไม่ได้หยุดอยู่ ให้ส่ง increment() ด้วย submit()
    • โมเดลแบบลำดับ counter_model ก็เพิ่มค่าด้วยจำนวนครั้งเท่ากัน
  • ท้ายสุดจะ join() thread ทั้งหมด และเปรียบเทียบ counter_model กับ counter.get() จริง

การทำงานของ pause และ unpause

  • pause() ใช้ thread_local! เพื่อค้นหา context ของ managed thread ปัจจุบัน โดยไม่ต้องเปลี่ยน API ของ Counter ที่ถูกทดสอบ
    • context ถูกแชร์ด้วย Arc<SharedContext>
    • SharedContext มี Mutex<State> และ Condvar
  • สถานะแบ่งเป็น Ready, Running, Paused
    • Ready: สถานะที่รอ closure ถัดไป
    • Running: สถานะที่ managed thread กำลังรัน
    • Paused: สถานะที่หยุดอยู่ ณ จุด pause()
  • เมื่อ managed thread มาถึง pause() จะเปลี่ยนสถานะจาก Running เป็น Paused และแจ้ง thread ควบคุมด้วย condition variable
  • unpause() เปลี่ยนสถานะจาก Paused เป็น Running และปลุก managed thread จากนั้นรอจนกว่าสถานะจะไม่ใช่ Running อีกครั้ง
    • ป้องกันสถานการณ์ที่ thread ควบคุมกับ managed thread รันต่อพร้อมกัน
    • ทำให้มีเพียงฝ่ายใดฝ่ายหนึ่งเท่านั้นที่รันในแต่ละขณะ เพื่อลด ความไม่แน่นอน

การทำซ้ำและย่อกรณีล้มเหลว

  • การรัน arbtest พบความล้มเหลวใน counter ที่เสีย
    • ตัวอย่างความล้มเหลวคือค่าโมเดล 4 แต่ค่าจริง 3
    • seed ที่ล้มเหลวคือ 0x4fd7ddff00000020
  • หากระบุ seed เดิม จะได้ interleaving เดิมอีกครั้ง ทำให้ทำซ้ำความล้มเหลวได้ง่าย
  • เมื่อใช้ .minimize() กรณีล้มเหลวจะถูกลดให้เหลือการรันที่สั้นลง
    • seed ของกรณีขั้นต่ำสุดท้ายคือ 0x9c2a13a600000001
    • trace ขั้นต่ำมีสี่ขั้น
      • 0: increment
      • 1: increment
      • 0: unpause
      • 1: unpause
  • ในกรณีขั้นต่ำนี้ ค่าที่คาดไว้คือ 2 แต่ค่าจริงเป็น 1 เผยให้เห็นข้อบกพร่องของการเพิ่มค่าที่อิง load/store

ขยายเป็นการไล่แจง interleaving ทั้งหมด

  • โครงสร้างเดียวกันสามารถเปลี่ยนจาก interleaving แบบสุ่มเป็นแบบไล่แจงได้
  • ใช้ exhaustigen เขียนการทดสอบที่สำรวจ interleaving ทั้งหมดจนถึงการเพิ่มค่าสูงสุด 5 ครั้ง
    • การทดสอบหลีกเลี่ยง loop dummy และจัดให้ thread ถูก unpause หรือส่ง increment เสมอ
  • implementation ที่เสียพบ bug เดิม
    • ตัวอย่างความล้มเหลวคือ left: 2, right: 1
  • เมื่อแก้ Counter::increment() เป็น fetch_add(1, SeqCst) การทดสอบก็ผ่าน
    • เพิ่ม pause() ก่อนและหลัง fetch_add() ใน wrapper AtomicU32 ด้วย
    • ผลการรันคือ all 81133 interleavings are fine!
    • เวลารันคือ real 8.65s, CPU 8.16s, RSS 63.91mb

การขยายไปสู่ weak memory model และ model checking

  • AtomicU32 ใน implementation ของเล่นตอนนี้ delegate ไปยัง atomic จริง
  • แนวคิดสำหรับขยายคือให้แต่ละ atomic เก็บเซตของค่าที่ถูกเขียนไว้ และเมื่ออ่านให้คืนค่าใดค่าหนึ่งที่สอดคล้องกับ weak memory model
  • การสำรวจ interleaving ก็สามารถทำให้ฉลาดกว่าการสุ่มได้
    • ใช้แนวทาง model checking เพื่อตรวจว่าได้พิจารณา interleaving ที่แตกต่างกันอย่างมีนัยสำคัญครบแล้วหรือไม่
    • ไล่แจง interleaving ทั้งหมดในขอบเขตเล็ก ๆ ได้ เช่นเดียวกับวิธีใน Generate All The Things

ทำไมจึงย่อให้เล็กได้โดยไม่ต้องมี shrinking

  • arbtest ที่ใช้ดูเหมือนอินเทอร์เฟซ PRNG ที่คุ้นเคย แต่ใช้ PRNG แบบมีขอบเขตจำกัด
    • หากขอค่าสุ่มต่อไปเรื่อย ๆ ถึงจุดหนึ่งจะคืน Err(OutOfEntropy)
    • ดังนั้นในโค้ดทดสอบจึงมี ? และ while !rng.is_empty()
  • เมื่อการทดสอบใช้ entropy หมด ก็จะจบสั้น ๆ ดังนั้นถ้าลด entropy ที่ใช้ได้ การรันทดสอบก็จะสั้นลงด้วย
  • implementation ภายในในเชิงแนวคิดใกล้เคียงกับ &mut &[u8]
    • ทุกครั้งที่ขอตัวเลขสุ่ม byte slice จะสั้นลง
    • slice เริ่มต้นยิ่งสั้น การทดสอบก็ยิ่งเรียบง่าย
  • ด้วยวิธีนี้ กรณีล้มเหลวจึงสั้นลงได้โดยไม่ต้อง implement logic สำหรับ shrinking แยกเอง
  • โค้ดต้นฉบับของตัวอย่างอยู่ที่ properly-concurrent

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-07-07
ความคิดเห็นจาก Hacker News

  • ใน Rust กำลังทำไลบรารีชื่อ Temper ด้วยแนวทางคล้ายกัน: https://github.com/reitzensteinm/temper/tree/main
    อย่างไรก็ตาม หากต้องการโมเดลนัยแปลก ๆ ที่เกิดจาก memory model ทั้งหมดของ Rust ต้องไปไกลกว่านี้มาก จึงจำเป็นต้องมีบัญชีติดตามว่าแต่ละเธรดรับรู้การเขียนใดไปแล้วบ้าง ตาม atomic memory ordering, read/write fence ฯลฯ อาจเกิดการรับประกันในทำนองว่า ถ้ารับรู้การเขียน X แล้ว ก็ต้องรับรู้การเขียน Y ด้วยเสมอ
    คิดว่าน่าจะเป็นชุดกรณีทดสอบ memory model ของ C++/Rust ที่รวบรวมไว้มากที่สุดแห่งหนึ่ง และแทบจะรวบรวมทุกอย่างที่หาได้จากหนังสือ มาตรฐาน C++, Stack Overflow, บล็อก ฯลฯ ไว้แล้ว ตัวอย่างเช่น ไฟล์สำหรับหนังสือ Rust Atomics and Locks ของ Mara Bos อยู่ที่นี่: https://github.com/reitzensteinm/temper/blob/main/memlog/tes...
    Loom ที่กล่าวถึงในบทความเป็นไลบรารีที่คล้ายกันแต่สมบูรณ์กว่ามาก ช่วยให้ทดสอบคอมโพเนนต์ระดับสูงกว่าอย่าง mutex หรือ queue ได้อย่างละเอียด: https://github.com/tokio-rs/loom อย่างไรก็ตาม ตัว memory model เองไม่ได้ถูกโมเดลอย่างถี่ยิบเท่า Temper และก็เคยคิดจะย้ายกรณีทดสอบไปใช้ Loom อยู่
    ได้แรงบันดาลใจจากงานนำเสนอการทดสอบ FoundationDB ของ Will Wilson และตอนนี้เขากำลังทำโซลูชันบนไฮเปอร์ไวเซอร์ที่ Antithesis เพื่อทดสอบคอนเทนเนอร์ Docker ใด ๆ ด้วยวิธีแบบนี้: https://www.youtube.com/watch?v=4fFDFbi3toc, https://antithesis.com/
    เชื่ออย่างหนักแน่นว่าอีก 10 ปีข้างหน้า พื้นที่นี้จะเติบโตขึ้นมาก WebAssembly อยู่ในจุดลงตัว คือสมบูรณ์พอที่จะคอมไพล์ซอฟต์แวร์ใด ๆ ได้ แต่ก็เรียบง่ายพอที่การสร้างสิ่งแบบ Antithesis จะไม่กลายเป็นโปรเจกต์ 5 ปีของทีมระดับหัวกะทิที่เคยออกฐานข้อมูลมาแล้ว

  • เคย implement atomic snapshot ของ shared memory ด้วย Rust และให้ความสำคัญกับการทดสอบอัตโนมัติอย่างจริงจังที่สุดเท่าที่ทำได้: https://github.com/kaymanb/todc/tree/main/todc-mem
    ตอนแรกใช้ Loom ที่อยู่ในบทความ แต่ภายหลังเปลี่ยนเป็น shuttle: https://github.com/tokio-rs/loom, https://github.com/awslabs/shuttle
    shuttle ใช้แนวทางแบบสุ่มแทนการสำรวจครบถ้วนเหมือน Loom แต่ตัว scheduler ก็ยังให้การรับประกันเชิงความน่าจะเป็นในการค้นพบบั๊ก จากที่ลองใช้ shuttle เร็วกว่าและขยายไปยังสถานการณ์ทดสอบที่ซับซ้อนกว่าได้
    คล้ายกับวิธีในบทความ เมื่อ schedule ใดทำให้การทดสอบล้มเหลว ก็สามารถบันทึก random seed ไว้ได้ ความสามารถในการทำซ้ำการทดสอบที่ล้มเหลวได้อย่างรวดเร็วนั้นสำคัญมาก และทำให้เขียน test case แบบชัดเจนสำหรับบั๊กที่เคยจับได้และแก้ไขไปแล้วได้: https://github.com/kaymanb/todc/blob/0e2874a70ec8beed8fae773...

  • ฝั่ง Kotlin/Java มี Lincheck ของ JetBrains เป็นไลบรารีที่ดีสำหรับงานแบบนี้: https://github.com/JetBrains/lincheck
    โดยเฉพาะชอบที่เป็นแบบ declarative และวิธีที่มันแสดงผลลัพธ์เรื่อง linearizability

  • สงสัยว่าใน C++ มีไลบรารีแบบ Loom ไหม มี โครงสร้างข้อมูลแบบ lock-free ที่อยากทดสอบอยู่

  • หากเข้าใจถูก แนวทางนี้มีข้อจำกัดเกี่ยวกับ การรับประกันความคืบหน้าแบบอ่อน
    การคำนวณในเนื้อหาหลักไม่ได้เล็กน้อยมากนัก แต่ในฮาร์ดแวร์จริงและสเกดจูลเลอร์จริง เราอาจนึกถึงลูป cmpxchg ที่มีโอกาสถูกหยุดบน CPU ใด CPU หนึ่งต่ำมาก หากจำนวน CPU คือ n ในกรณีเลวร้ายที่สุด ความน่าจะเป็นที่จะคืบหน้าคือ 1/n แต่ในวิธีทดสอบนี้จะกลายเป็น 1/t^p โดยที่ t คือจำนวนงาน ซึ่งอาจมากกว่าจำนวน CPU มาก และ p คือจำนวนครั้งที่หยุดชั่วคราวในตัวลูปนั้น ซึ่งกลายเป็น 3 หรือมากกว่าได้ง่าย ๆ ระดับนี้เพียงพอที่จะทำให้อัลกอริทึมที่ใช้งานได้จริงดูเหมือนพัง
    ในทางกลับกัน แม้ในกรณีที่ต้องการจับความคืบหน้าแบบอ่อนว่าเป็นบั๊ก จึงต้องการความคืบหน้าแบบแข็ง วิธีนี้ก็ดูไม่ได้ให้เครื่องมือที่มีประโยชน์นัก
    ถึงอย่างนั้น มันก็มีประโยชน์ชัดเจนกับปัญหา concurrency จำนวนมาก

    • 1/t^p ดูเหมือนจะไม่ถูก และน่าจะมองว่าเป็นแค่ 1/t มากกว่า สุดท้ายเมื่อเวลาผ่านไป t หนึ่ง งานใดงานหนึ่งย่อมต้องคืบหน้า และถ้ามีงาน t งาน ความน่าจะเป็นที่งานที่คืบหน้าจะเป็นงานของฉันก็คือ 1/t
      จุดสับสนหลักน่าจะอยู่ที่การถูกหยุดไม่ได้หมายความว่าจะต้องแพ้ที่ CAS เสมอไป

  • สำหรับส่วนที่ว่า “พูดตรง ๆ คือมีความรู้พื้นฐานบางอย่างอยู่ในนี้ เว้นแต่จะทำเรื่องต้องสาปมาก ๆ ด้วย inline assembly ดูเหมือนว่าเราจะหลีกเลี่ยงการสร้างเธรดจริงไม่ได้ หากมีอะไรบางอย่างเรียกฟังก์ชัน pause() และเราต้องการทำให้มันหยุดอยู่จนกว่าจะมีคำสั่งในภายหลัง งานนั้นจะต้องเกิดขึ้นภายในเธรดที่มีสแตกแยกจากสแตกของการทดสอบ” ผมสงสัยว่าใช้ async runtime บางชนิดไม่ได้หรือ
    ดูเหมือนเป็นการทำ cooperative multitasking ด้วยการ instrument atomic operation อาจต้องดื่มกาแฟเพิ่มอีกหน่อย แต่การทำโดยไม่มีเธรดดูจะง่ายกว่า

    • ถ้าใช้ async ก็คงสะดวก แต่ข้อกำหนดอีกอย่างคือเรา ไม่ต้องการเปลี่ยน API ที่สังเกตได้จากภายนอกของซอฟต์แวร์ที่ถูกทดสอบ async นั้น “แพร่เชื้อ” ได้ ดังนั้น API แบบ synchronous ก็ต้องใช้ implementation แบบ synchronous

  • ข้อเสียอย่างหนึ่งของแนวทางนี้คือ ต้อง แก้ไข โค้ดที่ถูกทดสอบเองให้เข้ากับโค้ดทดสอบ
    น่าจะทำสิ่งเดียวกันได้ด้วยการเปิดสองเธรด แล้วใช้ ptrace ทำ single-step พร้อมแทรกการรันคำสั่งแบบ “สุ่ม” คล้ายกับ chaos mode ของ rr
    อย่างไรก็ตาม บางคำสั่งอาจไม่เป็น atomic ดังนั้นถ้าเป็นไปได้โดยไม่ต้อง emulate ก็คงต้องมีวิธี single-step ในหน่วย “ไมโครโค้ดแบบ atomic”

    • ฟังดูเหมือน hypervisor ของ Antithesis

  • หากจะใช้ Loom ดูเหมือนต้องใช้ conditional compilation และแม้จะโอเคเมื่อทดสอบไลบรารีหนึ่งตัว แต่ก็ค่อนข้าง intrusive
    #[cfg(loom)]
    pub(crate) use loom::sync::atomic::AtomicUsize;
    #[cfg(not(loom))]
    pub(crate) use std::sync::atomic::AtomicUsize;
    สงสัยว่ามีภาษาที่ช่วยให้ใช้สเกดจูลเลอร์ของตัวเองได้ดีกว่านี้หรือไม่

  • ถ้าจะทำให้ละเอียดจริง ๆ น่าจะรันการทดสอบด้วย ptrace แล้วให้เธรดเดินแบบ single-step เพื่อสร้าง interleaving ที่ต่างกันในระดับคำสั่งได้ สงสัยว่าเคยเห็นวิธีแบบนั้นจริง ๆ ไหม
    ในกรณีที่ไม่สามารถ instrument โค้ดได้แบบนี้ มีทางเลือกสำหรับการทดสอบแบบ black-box หรือเปล่า?

    • ผมเคยใช้วิธีแบบนั้นกับการทดสอบ asynchronous signal handler แต่ฝั่งนั้นจำนวนชุดผสมเอื้อกว่ามาก หากเธรดหลักรันคำสั่ง n คำสั่ง ก็ต้องรันเพียง n ครั้ง โดยรันตั้งแต่ 0 ถึง n คำสั่งก่อนแทรกสัญญาณ จากนั้น signal handler รันจนจบ แล้วเธรดหลักก็รันจนจบ เวลารวมคือ O(n^2)
      แต่ถ้ามีเธรด t ตัวที่แต่ละตัวรันคำสั่ง n คำสั่ง และสามารถหยุดกันและกันได้ที่ทุกขอบเขต สำหรับค่า n ที่สมจริงแล้วคงเข้าถึงได้ยาก น่าจะต้องลดลงด้วยการเลือกเฉพาะ operation ที่มีพฤติกรรมน่าสนใจแล้วจำลองมัน

  • ดูค่อนข้างเจ๋ง น่าจะต้องลองใช้ดูสักครั้ง แต่คงจับข้อผิดพลาดไม่ได้ทุกชนิด การเรียก pause() ทุกครั้งจะสร้าง synchronization ระหว่างเธรด จนอาจบดบังปัญหา data race บางส่วนหรือเปล่า? ใน Rust อาจไม่ใช่ปัญหา