From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from bombadil.infradead.org (bombadil.infradead.org [198.137.202.133]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.lore.kernel.org (Postfix) with ESMTPS id CA87DC433F5 for ; Tue, 18 Jan 2022 12:34:36 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lists.infradead.org; s=bombadil.20210309; h=Sender: Content-Transfer-Encoding:Content-Type:List-Subscribe:List-Help:List-Post: List-Archive:List-Unsubscribe:List-Id:In-Reply-To:MIME-Version:References: Message-ID:Subject:Cc:To:From:Date:Reply-To:Content-ID:Content-Description: Resent-Date:Resent-From:Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID: List-Owner; bh=nFIJFuGbQrGChVN/INbIxtMv0KRBEDleo0ETARvt96o=; b=T4C+UOqMIQJaez iAEUgibPJ2L6ElQiMi/CJ9WQy+Zi24NLHRvSvKCdTyi7Hqp9wHM183tMjwKkA5BfgzWlfgIzrDNFx nDamTtFm1oAveT9dTJGOjjkx+V/tdIp3pVXocbOnj56zJLsUxFbV8DXc3Q2gx4NWfJ0y3c8c/coQZ Or+gcQvPfQj4pYyAOH5cNJR5pywjfxoXPniEx6jKyO81oVCDISwb+VlTJbEPXVwVOJalihBkQTcKE gPk7CkAPd1lf9dxfTK9n4x9gSaUCRTo4OcO/tCpF1+z+4Arh3DzLRepJyOcWFyMQ00BkvtPf8QjJ1 oSkNzwEkPoRUENbxG+BQ==; Received: from localhost ([::1] helo=bombadil.infradead.org) by bombadil.infradead.org with esmtp (Exim 4.94.2 #2 (Red Hat Linux)) id 1n9nff-001TmT-Bg; Tue, 18 Jan 2022 12:33:07 +0000 Received: from dfw.source.kernel.org ([2604:1380:4641:c500::1]) by bombadil.infradead.org with esmtps (Exim 4.94.2 #2 (Red Hat Linux)) id 1n9nfa-001Tm0-T4 for linux-arm-kernel@lists.infradead.org; Tue, 18 Jan 2022 12:33:04 +0000 Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 3CC7B613EA; Tue, 18 Jan 2022 12:33:02 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 0AF26C00446; Tue, 18 Jan 2022 12:32:58 +0000 (UTC) Date: Tue, 18 Jan 2022 12:32:55 +0000 From: Catalin Marinas To: Shameer Kolothum Cc: linux-arm-kernel@lists.infradead.org, kvmarm@lists.cs.columbia.edu, linux-kernel@vger.kernel.org, maz@kernel.org, will@kernel.org, james.morse@arm.com, julien.thierry.kdev@gmail.com, suzuki.poulose@arm.com, jean-philippe@linaro.org, Alexandru.Elisei@arm.com, qperret@google.com, jonathan.cameron@huawei.com, linuxarm@huawei.com Subject: Re: [PATCH v4 0/4] kvm/arm: New VMID allocator based on asid Message-ID: References: <20211122121844.867-1-shameerali.kolothum.thodi@huawei.com> MIME-Version: 1.0 Content-Disposition: inline In-Reply-To: <20211122121844.867-1-shameerali.kolothum.thodi@huawei.com> X-CRM114-Version: 20100106-BlameMichelson ( TRE 0.8.0 (BSD) ) MR-646709E3 X-CRM114-CacheID: sfid-20220118_043302_999710_7570EC2F X-CRM114-Status: GOOD ( 22.25 ) X-BeenThere: linux-arm-kernel@lists.infradead.org X-Mailman-Version: 2.1.34 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: "linux-arm-kernel" Errors-To: linux-arm-kernel-bounces+linux-arm-kernel=archiver.kernel.org@lists.infradead.org Hi Shameer, On Mon, Nov 22, 2021 at 12:18:40PM +0000, Shameer Kolothum wrote: > =A0-TLA+ model. Modified the asidalloc model to incorporate the new > VMID algo. The main differences are, > =A0 -flush_tlb_all() instead of local_tlb_flush_all() on rollover. > =A0 -Introduced INVALID_VMID and vCPU Sched Out logic. > =A0 -No CnP (Removed UniqueASIDAllCPUs & UniqueASIDActiveTask invariants). > =A0 -Removed =A0UniqueVMIDPerCPU invariant for now as it looks like > because of the speculative fetching with flush_tlb_all() there > is a small window where this gets triggered. If I change the > logic back to local_flush_tlb_all(), UniqueVMIDPerCPU seems to > be fine. With my limited knowledge on TLA+ model, it is not > clear to me whether this is a problem with the above logic > or the VMID model implementation. Really appreciate any help > with the model. > The initial VMID TLA+ model is here, > https://github.com/shamiali2008/kernel-tla/tree/private-vmidalloc-v1 I only had a brief look at the TLA+ model and I don't understand why you have a separate 'shed_out' process. It would run in parallel with the 'sched' but AFAICT you can't really schedule a guest out while you are in the middle of scheduling it in. I'd rather use the same 'sched' process and either schedule in an inactive task or schedule out an active one for a given CPU. Also active_vmids[] for example is defined on the CPUS domain but you call vcpu_sched_out() from a process that's not in the CPUS domain but the SCHED_OUT one. Regarding UniqueVMIDPerCPU, I think we need to figure out why it happens. The fact that flush_tlb_all() was made to simulate the speculative TLB loads is not relevant. In a different spec I have, arm64kpti.tla, I just used another process that invokes an update_tlbs() macro so that it can happen at any time. I didn't bother to update the ASID spec in a similar way but it may be useful. The corresponding UniqueASIDPerCPU meant that for any two TLB entries on a single CPU, if they correspond to different tasks (pgd), they should have different ASIDs. That's a strong requirement, otherwise we end up with the wrong translation. Why did you remove the CnP? Do we have this disabled for KVM guests? -- = Catalin _______________________________________________ linux-arm-kernel mailing list linux-arm-kernel@lists.infradead.org http://lists.infradead.org/mailman/listinfo/linux-arm-kernel