@@ -462,7 +462,7 @@ impl Queue {
462
462
// This fence ensures all descriptor writes are visible before the index update is.
463
463
fence ( Ordering :: Release ) ;
464
464
465
- self . set_next_used ( self . next_used . 0 , mem) ;
465
+ self . set_used_ring_idx ( self . next_used . 0 , mem) ;
466
466
Ok ( ( ) )
467
467
}
468
468
@@ -525,7 +525,7 @@ impl Queue {
525
525
526
526
/// Helper method that writes to the `avail_event` field of the used ring.
527
527
#[ inline( always) ]
528
- fn set_avail_event < M : GuestMemory > ( & mut self , avail_event : u16 , mem : & M ) {
528
+ fn set_used_ring_avail_event < M : GuestMemory > ( & mut self , avail_event : u16 , mem : & M ) {
529
529
debug_assert ! ( self . is_layout_valid( mem) ) ;
530
530
531
531
// Used ring has layout:
@@ -548,7 +548,7 @@ impl Queue {
548
548
549
549
/// Helper method that writes to the `idx` field of the used ring.
550
550
#[ inline( always) ]
551
- fn set_next_used < M : GuestMemory > ( & mut self , next_used : u16 , mem : & M ) {
551
+ fn set_used_ring_idx < M : GuestMemory > ( & mut self , next_used : u16 , mem : & M ) {
552
552
debug_assert ! ( self . is_layout_valid( mem) ) ;
553
553
554
554
// Used ring has layout:
@@ -596,9 +596,9 @@ impl Queue {
596
596
}
597
597
598
598
// Set the next expected avail_idx as avail_event.
599
- self . set_avail_event ( self . next_avail . 0 , mem) ;
599
+ self . set_used_ring_avail_event ( self . next_avail . 0 , mem) ;
600
600
601
- // Make sure all subsequent reads are performed after `set_avail_event `.
601
+ // Make sure all subsequent reads are performed after `set_used_ring_avail_event `.
602
602
fence ( Ordering :: SeqCst ) ;
603
603
604
604
// If the actual avail_idx is different than next_avail one or more descriptors can still
@@ -903,14 +903,14 @@ mod verification {
903
903
mod stubs {
904
904
use super :: * ;
905
905
906
- // Calls to set_avail_event tend to cause memory to grow unboundedly during verification.
907
- // The function writes to the `avail_event` of the virtio queue, which is not read
908
- // from by the device. It is only intended to be used by guest. Therefore, it does not
909
- // affect any device functionality (e.g. its only call site, try_enable_notification ,
910
- // will behave independently of what value was written here). Thus we can stub it out
911
- // with a no-op. Note that we have a separate harness for set_avail_event, to ensure
912
- // the function itself is sound.
913
- fn set_avail_event < M : GuestMemory > ( _self : & mut Queue , _val : u16 , _mem : & M ) {
906
+ // Calls to set_used_ring_avail_event tend to cause memory to grow unboundedly during
907
+ // verification. The function writes to the `avail_event` of the virtio queue, which
908
+ // is not read from by the device. It is only intended to be used by guest.
909
+ // Therefore, it does not affect any device functionality (e.g. its only call site,
910
+ // try_enable_notification, will behave independently of what value was written
911
+ // here). Thus we can stub it out with a no-op. Note that we have a separate harness
912
+ // for set_used_ring_avail_event, to ensure the function itself is sound.
913
+ fn set_used_ring_avail_event < M : GuestMemory > ( _self : & mut Queue , _val : u16 , _mem : & M ) {
914
914
// do nothing
915
915
}
916
916
}
@@ -1043,10 +1043,10 @@ mod verification {
1043
1043
1044
1044
#[ kani:: proof]
1045
1045
#[ kani:: unwind( 0 ) ]
1046
- fn verify_set_avail_event ( ) {
1046
+ fn verify_set_used_ring_avail_event ( ) {
1047
1047
let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
1048
1048
1049
- queue. set_avail_event ( kani:: any ( ) , & mem) ;
1049
+ queue. set_used_ring_avail_event ( kani:: any ( ) , & mem) ;
1050
1050
}
1051
1051
1052
1052
#[ kani:: proof]
@@ -1092,7 +1092,7 @@ mod verification {
1092
1092
1093
1093
#[ kani:: proof]
1094
1094
#[ kani:: unwind( 0 ) ]
1095
- #[ kani:: stub( Queue :: set_avail_event , stubs:: set_avail_event ) ]
1095
+ #[ kani:: stub( Queue :: set_used_ring_avail_event , stubs:: set_used_ring_avail_event ) ]
1096
1096
fn verify_try_enable_notification ( ) {
1097
1097
let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
1098
1098
@@ -1483,17 +1483,17 @@ mod tests {
1483
1483
}
1484
1484
1485
1485
#[ test]
1486
- fn test_set_avail_event ( ) {
1486
+ fn test_set_used_ring_avail_event ( ) {
1487
1487
let m = & default_mem ( ) ;
1488
1488
let vq = VirtQueue :: new ( GuestAddress ( 0 ) , m, 16 ) ;
1489
1489
1490
1490
let mut q = vq. create_queue ( ) ;
1491
1491
assert_eq ! ( vq. used. event. get( ) , 0 ) ;
1492
1492
1493
- q. set_avail_event ( 10 , m) ;
1493
+ q. set_used_ring_avail_event ( 10 , m) ;
1494
1494
assert_eq ! ( vq. used. event. get( ) , 10 ) ;
1495
1495
1496
- q. set_avail_event ( u16:: MAX , m) ;
1496
+ q. set_used_ring_avail_event ( u16:: MAX , m) ;
1497
1497
assert_eq ! ( vq. used. event. get( ) , u16 :: MAX ) ;
1498
1498
}
1499
1499
0 commit comments