@@ -462,7 +462,7 @@ impl Queue {
462462 // This fence ensures all descriptor writes are visible before the index update is.
463463 fence ( Ordering :: Release ) ;
464464
465- self . set_next_used ( self . next_used . 0 , mem) ;
465+ self . set_used_ring_idx ( self . next_used . 0 , mem) ;
466466 Ok ( ( ) )
467467 }
468468
@@ -525,7 +525,7 @@ impl Queue {
525525
526526 /// Helper method that writes to the `avail_event` field of the used ring.
527527 #[ 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 ) {
529529 debug_assert ! ( self . is_layout_valid( mem) ) ;
530530
531531 // Used ring has layout:
@@ -548,7 +548,7 @@ impl Queue {
548548
549549 /// Helper method that writes to the `idx` field of the used ring.
550550 #[ 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 ) {
552552 debug_assert ! ( self . is_layout_valid( mem) ) ;
553553
554554 // Used ring has layout:
@@ -596,9 +596,9 @@ impl Queue {
596596 }
597597
598598 // 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) ;
600600
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 `.
602602 fence ( Ordering :: SeqCst ) ;
603603
604604 // If the actual avail_idx is different than next_avail one or more descriptors can still
@@ -903,14 +903,14 @@ mod verification {
903903 mod stubs {
904904 use super :: * ;
905905
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 ) {
914914 // do nothing
915915 }
916916 }
@@ -1043,10 +1043,10 @@ mod verification {
10431043
10441044 #[ kani:: proof]
10451045 #[ kani:: unwind( 0 ) ]
1046- fn verify_set_avail_event ( ) {
1046+ fn verify_set_used_ring_avail_event ( ) {
10471047 let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
10481048
1049- queue. set_avail_event ( kani:: any ( ) , & mem) ;
1049+ queue. set_used_ring_avail_event ( kani:: any ( ) , & mem) ;
10501050 }
10511051
10521052 #[ kani:: proof]
@@ -1092,7 +1092,7 @@ mod verification {
10921092
10931093 #[ kani:: proof]
10941094 #[ 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 ) ]
10961096 fn verify_try_enable_notification ( ) {
10971097 let ProofContext ( mut queue, mem) = ProofContext :: bounded_queue ( ) ;
10981098
@@ -1483,17 +1483,17 @@ mod tests {
14831483 }
14841484
14851485 #[ test]
1486- fn test_set_avail_event ( ) {
1486+ fn test_set_used_ring_avail_event ( ) {
14871487 let m = & default_mem ( ) ;
14881488 let vq = VirtQueue :: new ( GuestAddress ( 0 ) , m, 16 ) ;
14891489
14901490 let mut q = vq. create_queue ( ) ;
14911491 assert_eq ! ( vq. used. event. get( ) , 0 ) ;
14921492
1493- q. set_avail_event ( 10 , m) ;
1493+ q. set_used_ring_avail_event ( 10 , m) ;
14941494 assert_eq ! ( vq. used. event. get( ) , 10 ) ;
14951495
1496- q. set_avail_event ( u16:: MAX , m) ;
1496+ q. set_used_ring_avail_event ( u16:: MAX , m) ;
14971497 assert_eq ! ( vq. used. event. get( ) , u16 :: MAX ) ;
14981498 }
14991499
0 commit comments