High Level Proof of The Correctness of Dirty Page Tracking

High Level Proof of The Correctness of Dirty Page Tracking

[Takuya Yoshikawa]

This is what I wanted to read before starting GET_DIRTY_LOG work: about
possible race between VCPU threads and GET_DIRTY_LOG thread.

Although most things look trivial, there seem to be some interesting assumptions
the correctness is based on including mmu lock usage.

	Takuya

===
About MMU Page Fault Path:
1. Set bit in dirty bitmap
2. Make spte writable
3. Guest re-execute the write

If GET_DIRTY_LOG is allowed to write protect the page between step 1 and 2,
that page will be made writable again at step 2 and the write at step 3 will
not be caught.  Since the userspace can process that page before step 3, the
written data may be lost.  To avoid this mmu lock must be held correctly in
both sides as the current implementation does.

When GET_DIRTY_LOG write protects the page between step 2 and 3, the userspace
will process that page before or after step 3.  If it is after step 3, the
userspace will see the written data normally.  If it is before step 3, the
write protection including corresponding TLB flush is already completed and
the write at step 3 will be caught again.  Since the next GET_DIRTY_LOG will
catch this data, this is safe. -- (*1)

Other timings are trivial.


About Emulation Write Path:
1. Write to the guest memory
2. Set bit in dirty bitmap

The only concern here is what will happen if the userspace gets the dirty log
between step 1 and 2.  In that case the userspace sees the bit is clean and
may not process that page.  To not lose the written data, GET_DIRTY_LOG must
be done at least once more so that we get the remaining dirty bit. -- (*2)


About (*1), (*2):
These are really safe because the userspace stops the VCPUs before doing the
final GET_DIRTY_LOG.

Re: High Level Proof of The Correctness of Dirty Page Tracking

[Xiao Guangrong]

On 03/31/2012 11:12 PM, Takuya Yoshikawa wrote:

> This is what I wanted to read before starting GET_DIRTY_LOG work: about
> possible race between VCPU threads and GET_DIRTY_LOG thread.
> 
> Although most things look trivial, there seem to be some interesting assumptions
> the correctness is based on including mmu lock usage.
> 
> 	Takuya
> 
> ===
> About MMU Page Fault Path:
> 1. Set bit in dirty bitmap
> 2. Make spte writable
> 3. Guest re-execute the write
> 
> If GET_DIRTY_LOG is allowed to write protect the page between step 1 and 2,
> that page will be made writable again at step 2 and the write at step 3 will
> not be caught.  Since the userspace can process that page before step 3, the
> written data may be lost.  To avoid this mmu lock must be held correctly in
> both sides as the current implementation does.
> 


Hmm, according to (*2), if we set the dirty bit after make spte writeable,
it should be safe without holding mmu-lock?

Re: High Level Proof of The Correctness of Dirty Page Tracking

[Takuya Yoshikawa]

On Sun, 01 Apr 2012 11:38:17 +0800
Xiao Guangrong <xiaoguangrong@linux.vnet.ibm.com> wrote:

> > About MMU Page Fault Path:
> > 1. Set bit in dirty bitmap
> > 2. Make spte writable
> > 3. Guest re-execute the write
> > 
> > If GET_DIRTY_LOG is allowed to write protect the page between step 1 and 2,
> > that page will be made writable again at step 2 and the write at step 3 will
> > not be caught.  Since the userspace can process that page before step 3, the
> > written data may be lost.  To avoid this mmu lock must be held correctly in
> > both sides as the current implementation does.
> > 
> 
> 
> Hmm, according to (*2), if we set the dirty bit after make spte writeable,
> it should be safe without holding mmu-lock?
> 

Yes, probably.

But I just checked the current code.
Not sure about your fast page fault path.

	Takuya