From mboxrd@z Thu Jan 1 00:00:00 1970 From: Xiao Guangrong Subject: Re: High Level Proof of The Correctness of Dirty Page Tracking Date: Sun, 01 Apr 2012 11:38:17 +0800 Message-ID: <4F77CDA9.2030800@linux.vnet.ibm.com> References: <20120401001255.62d558b570abed499bc06356@gmail.com> Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Cc: kvm@vger.kernel.org To: Takuya Yoshikawa Return-path: Received: from e23smtp08.au.ibm.com ([202.81.31.141]:45033 "EHLO e23smtp08.au.ibm.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1754265Ab2DADiY (ORCPT ); Sat, 31 Mar 2012 23:38:24 -0400 Received: from /spool/local by e23smtp08.au.ibm.com with IBM ESMTP SMTP Gateway: Authorized Use Only! Violators will be prosecuted for from ; Sun, 1 Apr 2012 03:35:50 +1000 Received: from d23av04.au.ibm.com (d23av04.au.ibm.com [9.190.235.139]) by d23relay03.au.ibm.com (8.13.8/8.13.8/NCO v10.0) with ESMTP id q313cI1d1200220 for ; Sun, 1 Apr 2012 13:38:18 +1000 Received: from d23av04.au.ibm.com (loopback [127.0.0.1]) by d23av04.au.ibm.com (8.14.4/8.13.1/NCO v10.0 AVout) with ESMTP id q313cI2g006265 for ; Sun, 1 Apr 2012 13:38:18 +1000 In-Reply-To: <20120401001255.62d558b570abed499bc06356@gmail.com> Sender: kvm-owner@vger.kernel.org List-ID: 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?