Semaphore: đặt trước số key và kiểm cân bằng resource

Có hai key không có nghĩa mọi công việc được chạy đôi

Một pool có hai key. Nếu mỗi worker cần một key, hai worker có thể cùng dùng resource; nếu mỗi worker cần hai key, chỉ một worker được vào critical section. Số key biểu diễn đơn vị tài nguyên mà testbench quy ước, không tự biết một object hay một transaction cần bao nhiêu đơn vị.

Main cho mỗi worker lấy cả hai key để kiểm mutual exclusion. Nó kiểm cả thời điểm waiter được giải phóng lẫn ledger key cuối, vì chỉ thấy các worker in “done” chưa đủ biết chúng đã trả thiếu hoặc trả thừa resource.

Semaphore là object có state, handle không clone pool

semaphore pool=new(2) tạo một object với hai key ban đầu. Hai biến handle cùng nhận pool sẽ điều khiển cùng state ấy. Không new một semaphore riêng trong mỗi worker nếu mục tiêu là chia sẻ khóa, vì như vậy mỗi worker có một pool riêng và chẳng có mutual exclusion chung.

Main tạo đúng một pool ở top và cho cả hai branch dùng nó. Không có phần cứng khóa được tổng hợp ở đây: semaphore là cơ chế đồng bộ của testbench mô phỏng. Nhãn simulated không được dùng để suy netlist hoặc mức song song của chip thật.

^[1]

Get chờ đủ key rồi lấy, try_get không chờ

Get(n) là task có thể chặn cho tới khi lấy đủ n key. Try_get(n) là function trả ngay; khi thành công nó cũng lấy key, không chỉ nhìn xem resource có rảnh. Vì vậy một try_get dùng làm “kiểm thử” nhưng quên put trả lại vẫn có thể làm worker khác bị kẹt.

Trong preflight, main lấy hai key bằng try_get và yêu cầu lần lấy thêm một key thất bại. Nó trả một key, lấy lại một key ấy, rồi trả hai để phục hồi state ban đầu. Những lệnh này kiểm side effect, không chạy một loop polling bận để chờ resource.

^[2]

Viết ledger trước khi chạy hai worker

Sau new, pool có 2. Lấy 2 còn 0; thử lấy 1 thất bại vẫn 0; trả 1 thành 1; lấy 1 thành 0; trả 2 trở về 2. Đây là bước chuẩn bị có chủ đích trước pha blocking, không phải các con số được điều chỉnh theo output simulator.

Testbench nên gắn số key được trả với số key đã lấy theo contract của component. Semaphore không giữ một bảng ownership theo tên worker để tự phát hiện worker trả nhầm. Ledger trong oracle giúp nhìn được thiếu/thừa key mà chỉ kiểm một cờ active có thể bỏ sót.

Waiter đến 1 ns, chỉ lấy đủ hai key ở 3 ns

Holder lấy 2 ở 0 ns và giữ tới 3 ns. Waiter thử get(2) ở 1 ns nên phải chặn; sau holder trả 2 ở 3 ns nó mới vào, giữ thêm 1 ns và trả ở 4 ns. Main kiểm waiter_time=3, số acquire/release đều 2 và không lúc nào có hơn một worker trong critical section.

Chỉ có một waiter trong scenario này. Nó không chứng minh chính sách fairness giữa nhiều waiter có nhu cầu key khác nhau, cũng không ghim một thứ tự worker đồng thời đến chỉ dựa vào tên hoặc thứ tự dòng source. Để kiểm fairness cần scenario và oracle khác, được đối chiếu chuẩn riêng.

Số key ban đầu không phải capacity bất biến

Probe độc lập tạo semaphore với 1 key rồi put(2); nó lấy được 3 key và lần lấy thêm 1 thất bại. Kết quả này cho thấy put có thể tăng số key vượt mức ban đầu. Không coi new(2) là một guard tự động chống việc trả 3.

Trong main, contract vẫn là hai key cân bằng. Mutant holder trả 3 làm ledger cuối phát hiện dư key; mutant trả 1 khiến waiter đòi 2 không tiến được và watchdog dừng. Chỉ đổi capacity kỳ vọng để chấp nhận trả thừa sẽ che bug quản lý resource, nên checker được giữ nguyên.

Hủy worker không tự trả key nó đang giữ

Một worker bị disable hoặc kill sau get không mặc nhiên thực hiện đoạn put nằm phía sau. Nếu testbench dùng timeout cancellation, cần thiết kế nơi sở hữu ledger và cách cleanup, thay vì cho mỗi nhánh tự đoán còn bao nhiêu key.

Main không cố tình kill holder; nó kiểm lifecycle get/put hoàn tất bình thường. Liên hệ với bài fork là một yêu cầu thiết kế, không phải claim đã chạy mọi tình huống hủy/resource recovery. Cũng đừng thêm put vô điều kiện trong timeout mà chưa biết nhánh kia đã trả hay chưa: cách đó có thể biến thiếu key thành over-release.

Năm oracle và một ledger cuối

Expected trước chạy: SEMAPHORE CHECK checks=5 acquires=2 releases=2 max_active=1 waiter_ns=3 time_ns=4. Main parse/simulate trên Verilator; extra-key probe là positive case riêng, còn thiếu/thừa key là hai runtime fault riêng.

`timescale 1ns/1ps// Expected2keys, one blocking waiter released3ns, each branch releases exactly its acquired keys.module tb_semaphore; semaphore pool=new(2); int checks=0,active=0,max_active=0,acquires=0,releases=0,waiter_time=-1; initial begin  if(pool.try_get(2)!=1)$fatal(1,"semaphore initial keys oracle");checks++;  if(pool.try_get(1)!=0)$fatal(1,"semaphore exhausted oracle");checks++;  pool.put(1);  if(pool.try_get(1)!=1)$fatal(1,"semaphore partial return oracle");checks++;  pool.put(2);  fork   begin    pool.get(2);active++;acquires++;if(active>max_active)max_active=active;    #3;active--;releases++;pool.put(2);   end   begin    #1;pool.get(2);waiter_time=int'($time);active++;acquires++;if(active>max_active)max_active=active;    if(waiter_time!=3||active!=1)$fatal(1,"semaphore exclusive wait oracle");checks++;    #1;active--;releases++;pool.put(2);   end  join  if(pool.try_get(2)!=1||pool.try_get(1)!=0)$fatal(1,"semaphore final key ledger oracle");checks++;  pool.put(2);  if(checks!=5||active!=0||max_active!=1||acquires!=2||releases!=2||$time!=4)$fatal(1,"semaphore accounting");  $display("SEMAPHORE CHECK checks=5 acquires=2 releases=2 max_active=1 waiter_ns=3 time_ns=4");$finish; end initial begin #20;$fatal(1,"semaphore watchdog");endendmodule

Số check không đại diện cho mọi policy arbitration. Scope gồm preflight try_get, một holder/một waiter và cân bằng cuối; không claim fairness tổng quát, tự cleanup hoặc synthesis.

^[3]

Tự kiểm tra

Kiểm key, ownership và đường thoát

Hãy ghi mỗi worker cần bao nhiêu key, ai chịu trách nhiệm trả và điều gì xảy ra nếu worker không đi tới cuối. Kiểm try_get theo cả return value lẫn side effect, dùng ledger cuối để bắt over-release và giữ watchdog cho deadlock. Một khóa đúng cú pháp chưa phải một lifecycle đúng.