Mailbox: backpressure, FIFO và identity của transaction được gửi

Đã gửi handle chưa có nghĩa đã lưu bản chụp dữ liệu

Producer đưa một transaction vào mailbox rồi sửa object để tái sử dụng. Consumer có thể nhận handle trỏ đúng object đó nhưng thấy dữ liệu mới, không phải dữ liệu lúc put. Một FIFO đúng thứ tự vẫn có thể truyền một lịch sử sai nếu ownership của object không rõ.

Bài dùng hai pha: mailbox int có bound 2 để kiểm backpressure/FIFO, rồi mailbox Packet để kiểm identity và một snapshot tạo object riêng. Cần hiểu cả đồng bộ lẫn giá trị thực sự đi qua kênh; không ghép chúng thành một lời hứa “mailbox tự copy transaction”.

Mailbox object và kiểu message là hai thông tin khác

mailbox #(int) channel=new(2) tạo một object mailbox chứa int, tối đa hai message đang chờ. Hai handle cùng trỏ channel dùng chung queue nội bộ. Bound 0 nghĩa không đặt giới hạn message theo cơ chế bounded mailbox, không có nghĩa queue luôn rỗng.

Type parameter giúp kiểm việc đưa/nhận kiểu dữ liệu phù hợp. Nó không đặt ownership cho class object và không thay một comparator semantic. Bài dùng int cho phép tính và Packet chỉ có một field int để việc snapshot rõ; không claim mọi generic mixed-type mailbox hoặc deep-copy graph phức tạp.

^[1]

Put có thể chặn khi đầy, get có thể chặn khi rỗng

Pha blocking bắt đầu khi mailbox rỗng. Producer put 21 rồi 22 ở 0 ns, làm đầy hai slot. Ở 1 ns, put 23 phải chặn vì chưa có consumer lấy đi. Consumer bắt đầu get ở 3 ns, nhận 21 và mở chỗ để put 23 hoàn tất ở 3 ns.

Consumer lấy 22 ở 4 ns rồi 23 ở 5 ns. Tổng dự kiến 66; main kiểm từng value theo vị trí trước khi cộng. Một producer và một consumer được dùng để thứ tự gửi tường minh. Không suy thứ tự giữa nhiều producer cùng put ở một timestamp từ log của scenario này.

Try method báo kết quả của chính thao tác, không đặt reservation ngầm

Preflight dùng try_get khi rỗng và kiểm target còn 99, rồi try_put7/11 thành công và try_put13 thất bại do đầy. Try_peek nhìn thấy 7 nhưng num vẫn 2; try_get sau đó lần lượt lấy 7/11 và làm num giảm. Sau khi drain, một try_get thất bại phải giữ target 23.

Main kiểm success bằng giá trị trả về dương, không ghim số dương cụ thể thành quy tắc ngôn ngữ cho mọi tool. Num là một snapshot của occupancy, không phải reservation cho lần get tiếp theo: nếu có consumer khác xen vào, “num>0 rồi get” vẫn có thể chặn. Khi cần quyết định không chặn, dùng return code của chính try_get.

^[2]

Oracle theo vị trí, không chỉ theo tổng

Consumer yêu cầu value bằng 21+k với k 0..2. Nếu producer đổi thứ tự thành 22,21,23, tổng vẫn 66 nhưng FIFO-order oracle phải báo sai. Đây là lý do giữ từng phép so sánh thay vì chỉ tính checksum cuối rồi kết luận thứ tự đúng.

Main cũng kiểm put_release_time=3 và occupancy cuối 0. Những điều kiện này phát hiện một đường thực thi có dữ liệu đúng nhưng không có backpressure mong muốn. Mutant tăng bound từ 2 thành 3 bị preflight/full-capacity oracle bắt; không đổi expected để gọi cấu hình sai là cùng một scenario.

Message là class handle thì identity được chia sẻ

Packet sent được tạo với value 7 và put vào objects. Sender sửa sent.value thành 9 trước khi peek. Main yêu cầu peeked==sent và value 9: mailbox giữ giá trị handle trỏ cùng object, không tự chụp field 7 ở lúc put.

Tiếp theo sửa peeked.value thành 11 rồi get: received vẫn là cùng object với sent và sender cũng thấy 11. Peek không lấy message ra nhưng handle nó trả về vẫn có thể dùng để sửa object. “Chỉ quan sát queue” không đồng nghĩa object được bảo vệ readonly.

Không chuyển kết luận này sang int: với int, giá trị message được truyền theo value, không có một object dùng chung để sửa field qua alias. Kiểu của payload quyết định tầng identity cần review.

Snapshot của field nguyên thủy cần object riêng

Main tạo snapshot=new(sent.value) khi sent.value=11, rồi put snapshot và đổi sent.value thành 13. Consumer phải nhận snapshot khác identity với sent, value 11, trong khi sent giữ 13. Đây là copy một field nguyên thủy vào object mới, không phải deep clone tự động.

Mutant snapshot=sent chỉ tạo alias; sau sửa sender, received cũng thấy 13 và oracle snapshot phải bắt. Nếu Packet có nested handle/dynamic collection, cần một chính sách copy riêng và test thêm từng tầng như bài B5.copy; source hiện tại không được dùng làm proof cho mọi clone transaction.

12 oracle gồm cả kênh int và class

Expected trước chạy: MAILBOX CHECK checks=12 received=3 sum=66 put_release_ns=3 shared_value=11 copied_value=11 time_ns=5. Hai pha class không tiêu thụ thời gian nên kết thúc vẫn 5 ns của pha int.

`timescale 1ns/1ps// Expected try operations preserve target on empty; blocking put waits from1ns to3ns.class Packet; int value; function new(int v);value=v;endfunctionendclassmodule tb_mailbox; mailbox #(Packet) objects=new; Packet sent,peeked,received,snapshot; mailbox #(int) channel=new(2); int value=99,rc,checks=0,received_sum=0,release_time=-1; initial begin  rc=channel.try_get(value);if(rc!=0||value!=99)$fatal(1,"empty mailbox target oracle");checks++;  if(channel.try_put(7)<=0||channel.try_put(11)<=0||channel.try_put(13)!=0||channel.num()!=2)$fatal(1,"bounded mailbox try-put oracle");checks++;  if(channel.try_peek(value)<=0||value!=7||channel.num()!=2)$fatal(1,"mailbox peek oracle");checks++;  if(channel.try_get(value)<=0||value!=7||channel.num()!=1)$fatal(1,"mailbox first-get oracle");checks++;  if(channel.try_get(value)<=0||value!=11||channel.num()!=0)$fatal(1,"mailbox second-get oracle");checks++;  value=23;if(channel.try_get(value)!=0||value!=23)$fatal(1,"empty mailbox after drain oracle");checks++;  fork   begin    channel.put(21);channel.put(22);#1;channel.put(23);release_time=int'($time);    if(release_time!=3)$fatal(1,"mailbox blocking put release oracle");   end   begin    #3;    for(int k=0;k<3;k++)begin     channel.get(value);     if(value!=21+k)$fatal(1,"mailbox FIFO order oracle");     received_sum+=value;checks++;     if(k<2)#1;    end   end  join  sent=new(7);objects.put(sent);sent.value=9;  objects.peek(peeked);  if(peeked!=sent||peeked.value!=9||objects.num()!=1)$fatal(1,"mailbox handle identity oracle");checks++;  peeked.value=11;objects.get(received);  if(received!=sent||sent.value!=11||objects.num()!=0)$fatal(1,"mailbox handle shared-state oracle");checks++;  snapshot=new(sent.value);objects.put(snapshot);sent.value=13;objects.get(received);  if(received!=snapshot||received==sent||received.value!=11||sent.value!=13)$fatal(1,"mailbox explicit snapshot oracle");checks++;  if(checks!=12||received_sum!=66||channel.num()!=0||$time!=5)$fatal(1,"mailbox accounting");  $display("MAILBOX CHECK checks=12 received=3 sum=66 put_release_ns=3 shared_value=11 copied_value=11 time_ns=5");$finish; end initial begin #20;$fatal(1,"mailbox watchdog");endendmodule

Ba mutant giữ nguyên oracle: bound 3 thay 2, đảo hai message đầu và alias thay snapshot. Main parse/simulate trên Verilator; không claim nhiều producer, fairness, mọi mixed-type runtime hoặc clone object graph.

^[3]

Tự kiểm tra

Review kênh, thứ tự và ownership của payload

Khi debug producer/consumer, kiểm họ dùng cùng mailbox object, bound đúng, blocking point đúng và message đúng thứ tự. Sau đó xem payload là value hay handle, ai còn quyền sửa nó và snapshot được tạo ở đâu. Bảo toàn FIFO không thay cho bảo toàn dữ liệu transaction.