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

[Xiao Guangrong <xiaoguangrong@linux.vnet.ibm.com>]

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?