@@ -452,7 +452,7 @@ impl Queue {
452
452
// This fence ensures all descriptor writes are visible before the index update is.
453
453
fence ( Ordering :: Release ) ;
454
454
455
- self . set_next_used ( self . next_used . 0 , mem) ;
455
+ self . set_used_ring_idx ( self . next_used . 0 , mem) ;
456
456
Ok ( ( ) )
457
457
}
458
458
@@ -519,7 +519,7 @@ impl Queue {
519
519
}
520
520
521
521
/// Helper method that writes `val` to the `avail_event` field of the used ring.
522
- fn set_avail_event < M : GuestMemory > ( & mut self , val : u16 , mem : & M ) {
522
+ fn set_used_ring_avail_event < M : GuestMemory > ( & mut self , val : u16 , mem : & M ) {
523
523
debug_assert ! ( self . is_layout_valid( mem) ) ;
524
524
525
525
// Used ring has layout:
@@ -540,7 +540,7 @@ impl Queue {
540
540
mem. write_obj ( val, avail_event_addr) . unwrap ( ) ;
541
541
}
542
542
543
- fn set_next_used < M : GuestMemory > ( & mut self , val : u16 , mem : & M ) {
543
+ fn set_used_ring_idx < M : GuestMemory > ( & mut self , val : u16 , mem : & M ) {
544
544
debug_assert ! ( self . is_layout_valid( mem) ) ;
545
545
546
546
// Used ring has layout:
@@ -552,8 +552,8 @@ impl Queue {
552
552
// }
553
553
// We calculate offset into `idx` field.
554
554
let idx_offset = std:: mem:: size_of :: < u16 > ( ) ;
555
- let next_used_addr = self . used_ring . unchecked_add ( usize_to_u64 ( idx_offset) ) ;
556
- mem. write_obj ( val, next_used_addr ) . unwrap ( ) ;
555
+ let idx_addr = self . used_ring . unchecked_add ( usize_to_u64 ( idx_offset) ) ;
556
+ mem. write_obj ( val, idx_addr ) . unwrap ( ) ;
557
557
}
558
558
559
559
/// Try to enable notification events from the guest driver. Returns true if notifications were
@@ -588,9 +588,9 @@ impl Queue {
588
588
}
589
589
590
590
// Set the next expected avail_idx as avail_event.
591
- self . set_avail_event ( self . next_avail . 0 , mem) ;
591
+ self . set_used_ring_avail_event ( self . next_avail . 0 , mem) ;
592
592
593
- // Make sure all subsequent reads are performed after `set_avail_event `.
593
+ // Make sure all subsequent reads are performed after `set_used_ring_avail_event `.
594
594
fence ( Ordering :: SeqCst ) ;
595
595
596
596
// If the actual avail_idx is different than next_avail one or more descriptors can still
@@ -895,14 +895,14 @@ mod verification {
895
895
mod stubs {
896
896
use super :: * ;
897
897
898
- // Calls to set_avail_event tend to cause memory to grow unboundedly during verification.
899
- // The function writes to the `avail_event` of the virtio queue, which is not read
900
- // from by the device. It is only intended to be used by guest. Therefore, it does not
901
- // affect any device functionality (e.g. its only call site, try_enable_notification ,
902
- // will behave independently of what value was written here). Thus we can stub it out
903
- // with a no-op. Note that we have a separate harness for set_avail_event, to ensure
904
- // the function itself is sound.
905
- fn set_avail_event < M : GuestMemory > ( _self : & mut Queue , _val : u16 , _mem : & M ) {
898
+ // Calls to set_used_ring_avail_event tend to cause memory to grow unboundedly during
899
+ // verification. The function writes to the `avail_event` of the virtio queue, which
900
+ // is not read from by the device. It is only intended to be used by guest.
901
+ // Therefore, it does not affect any device functionality (e.g. its only call site,
902
+ // try_enable_notification, will behave independently of what value was written
903
+ // here). Thus we can stub it out with a no-op. Note that we have a separate harness
904
+ // for set_used_ring_avail_event, to ensure the function itself is sound.
905
+ fn set_used_ring_avail_event < M : GuestMemory > ( _self : & mut Queue , _val : u16 , _mem : & M ) {
906
906
// do nothing
907
907
}
908
908
}
@@ -1035,10 +1035,10 @@ mod verification {
1035
1035
1036
1036
#[ kani:: proof]
1037
1037
#[ kani:: unwind( 0 ) ]
1038
- fn verify_set_avail_event ( ) {
1038
+ fn verify_set_used_ring_avail_event ( ) {
1039
1039
let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
1040
1040
1041
- queue. set_avail_event ( kani:: any ( ) , & mem) ;
1041
+ queue. set_used_ring_avail_event ( kani:: any ( ) , & mem) ;
1042
1042
}
1043
1043
1044
1044
#[ kani:: proof]
@@ -1084,7 +1084,7 @@ mod verification {
1084
1084
1085
1085
#[ kani:: proof]
1086
1086
#[ kani:: unwind( 0 ) ]
1087
- #[ kani:: stub( Queue :: set_avail_event , stubs:: set_avail_event ) ]
1087
+ #[ kani:: stub( Queue :: set_used_ring_avail_event , stubs:: set_used_ring_avail_event ) ]
1088
1088
fn verify_try_enable_notification ( ) {
1089
1089
let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
1090
1090
@@ -1475,17 +1475,17 @@ mod tests {
1475
1475
}
1476
1476
1477
1477
#[ test]
1478
- fn test_set_avail_event ( ) {
1478
+ fn test_set_used_ring_avail_event ( ) {
1479
1479
let m = & default_mem ( ) ;
1480
1480
let vq = VirtQueue :: new ( GuestAddress ( 0 ) , m, 16 ) ;
1481
1481
1482
1482
let mut q = vq. create_queue ( ) ;
1483
1483
assert_eq ! ( vq. used. event. get( ) , 0 ) ;
1484
1484
1485
- q. set_avail_event ( 10 , m) ;
1485
+ q. set_used_ring_avail_event ( 10 , m) ;
1486
1486
assert_eq ! ( vq. used. event. get( ) , 10 ) ;
1487
1487
1488
- q. set_avail_event ( u16:: MAX , m) ;
1488
+ q. set_used_ring_avail_event ( u16:: MAX , m) ;
1489
1489
assert_eq ! ( vq. used. event. get( ) , u16 :: MAX ) ;
1490
1490
}
1491
1491
0 commit comments