From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 258DF282F26 for ; Thu, 18 Jun 2026 08:13:57 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1781770440; cv=none; b=I8o0M3kE2OUUszj9uULjq7yjt00Mpdw09PG1ThwMGrgstZffdyn/ox1n+4BU78zoI6lQGb/dS5muBaXYtUf1Lo9whR/vyDbUDn06OP6o7F7zg79oK9fINlmhl9ug4q1jvM0Xq/3b3SIlbcfs74xRpeYsXDpRgdgsK1XcAJAuArw= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1781770440; c=relaxed/simple; bh=V4atjPoRLxPj/P/o9GCbq2G6p0+PCrf2LHSnCgfA5UY=; h=Message-ID:Subject:From:To:Cc:Date:In-Reply-To:References: Content-Type:MIME-Version; b=NkA2NBTgKC239p3HOGNBiwGiLD5s2nV0LexL6RFSmNBmGD+/NLPrAmJVkdOByF6UVDJQwUE+0UB1oSlL8Tk9GcxiDN+iu9ARtOo+c6XlkD4IX9qKOFJJl8yg93Vcf3/LzzEwCwODjl0oJ0VqNTprXZMmdX/PZFipcpsqQDenOzk= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=Q9+FobWf; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b=ffZ4WXzy; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="Q9+FobWf"; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b="ffZ4WXzy" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1781770436; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=JMNQ/q7fbi4PfAmfawMCfx/QWCOmT+5njtbain3KxO8=; b=Q9+FobWff3GBn11rL5ynatUVX/XL1DOeiJTUpxEIRZfe5+2I4OABiQpH5sYyWE0xdL49/A aOiE2H+hW6JvVTLiv2POEPB3CNuyT1KGfGw/Lz1ppED6qXtOueDNEHzNIR6GiG9mceBp75 mwbfaSzUPGSycwAjOla0YtZORgc+pd4= Received: from mail-wr1-f70.google.com (mail-wr1-f70.google.com [209.85.221.70]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-207-ilWxLQ8tNbu81xTzMD-5hw-1; Thu, 18 Jun 2026 04:13:55 -0400 X-MC-Unique: ilWxLQ8tNbu81xTzMD-5hw-1 X-Mimecast-MFC-AGG-ID: ilWxLQ8tNbu81xTzMD-5hw_1781770434 Received: by mail-wr1-f70.google.com with SMTP id ffacd0b85a97d-45ef4931de5so1138280f8f.1 for ; Thu, 18 Jun 2026 01:13:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=google; t=1781770434; x=1782375234; darn=vger.kernel.org; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc:subject :date:message-id:reply-to; bh=JMNQ/q7fbi4PfAmfawMCfx/QWCOmT+5njtbain3KxO8=; b=ffZ4WXzyqO+xQRSz7jiO/d7Md8ahy8LKwz6jMbAFYuMLhWDsGQhZ3WfaJ7ycSXDx4d TRWHbmpY0BJpIoET+bfJcec73l7mRr83t1vGTxFKoJK0JtqhbQDoM4d+0L8mFr4S6vlH oedh0UVv7rI4ER00p6zol7X2iN4L97DBCcG9ulhpuTEKWh1XPffdLOX9S97KfDMjlnti HVEXdlyj82wLHkJ1CdUNQtlqiwbcTyBZqAlUY+9NOYoc66cBnoX/KYYjXqJq3OthWh5E oFL4pEH7pU5yrDlK77UPCO2I0NNI/tNjISbF/S4V6VhIVS/VfMoip4epcyDgNtucEKoV p67A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1781770434; x=1782375234; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-gg :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=JMNQ/q7fbi4PfAmfawMCfx/QWCOmT+5njtbain3KxO8=; b=HlaRJeQ3+uSrExPowZdzWn9pFc2z5sQ33MzxvwTmaxiYS4BO8bv50UnL1OcSQtZvh9 Qejv6wrTvHTzPR9EXNYv0X8i7L+jnnrcrQHN6JUBMkvtYgQ9tyaGhx1EL8vcWyHhkeuN sXlPoKDl/gDVyPyxr6xrT4zHS1bkGdudikjzdOZWPuq9vb7l+mcU5jd4keqlyoWY3Gpp eiX3W8BultoWj/vhr4Rgks739iubFHYiWPc/DI6zTsw+Df/7yxddkv0bM9sEZ4DqthPH 8fsjQTHiz7qLuyXdsEj6oCFb7DVxnaemg6CQ/Wk7vJExdQRDWN19tbvDlPQzoR728tHy rDrA== X-Forwarded-Encrypted: i=1; AFNElJ9WWedzlKcMi6LdRNnguMQ5clgXi691P7tCdcLhVmwpMFNUYI6Kv+kcFsgx0Vls9Oh5MP+t33L7fmgLuDg=@vger.kernel.org X-Gm-Message-State: AOJu0Yw/WdoWNj6Nv6K36/mcc7xyage5iOc7FpJOzgbplH+H6eRiqY7J Dog21G0+7d+QwMtwKTyTInbReLPk0jYM/lk8H7D1YSDcblxQHUZhxWpRL6IZImuXCPZ9hM+IOp7 yTYKRLgG6r995+PrnDhEJ3bSvXuTSaN1jjgz/iEmB2NBOGYGaDpIY62HPK7URn8XSsg== X-Gm-Gg: AfdE7cmu9BxJ+hWN4IHsn+drwbzQKASxigSZpBMYBXnR5w1Vc7Q8sHYmMqvUNwT6AF+ KqUXnmPLR9UVNVGOoyCRMXAX6SrZCMtvUZEzTd6MVVqKxWwMm1hzwCqf1ROE3azOTkKjJ02y1vA ZuozF01NhGIcFIQgd9YE1MFgY1PyuT2PTdEyhicFMBsfNo8be0xbFhAWnJw/mAqCM3B4WCA/JCz d9lXbZibR0/026sqTicc96XevyZL+hDAG1CrrSU8fYAaEdqkIFbk2n7g+gn3iDOPjGv18s8VQZZ q9g9X0gA4gO2cQto1f14Mbox+kpsx9tjsS2wzl760cjnn+KVTWm0yFcLre/lce/+jN9K+MjFHNa tefhKS7zfRhXKDyk= X-Received: by 2002:a05:6000:2989:20b0:462:6fdc:8194 with SMTP id ffacd0b85a97d-4639881b88fmr3232284f8f.25.1781770433943; Thu, 18 Jun 2026 01:13:53 -0700 (PDT) X-Received: by 2002:a05:6000:2989:20b0:462:6fdc:8194 with SMTP id ffacd0b85a97d-4639881b88fmr3232260f8f.25.1781770433508; Thu, 18 Jun 2026 01:13:53 -0700 (PDT) Received: from [192.168.1.167] ([185.168.96.228]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-4606f26392esm60856772f8f.3.2026.06.18.01.13.51 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 18 Jun 2026 01:13:52 -0700 (PDT) Message-ID: <9035cc5b83dda3a8ec06e8488fba62ceb7431123.camel@redhat.com> Subject: Re: [PATCH v3 09/13] verification/rvgen: Delete __parse_constraint() From: Gabriele Monaco To: Nam Cao Cc: Steven Rostedt , Wander Lairson Costa , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Date: Thu, 18 Jun 2026 10:13:50 +0200 In-Reply-To: <87tsr1mqrj.fsf@yellow.woof> References: <8d9b9068a5dde8256edd7debe7aab33e15a7fc51.1780908661.git.namcao@linutronix.de> <87tsr1mqrj.fsf@yellow.woof> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.60.2 (3.60.2-1.fc44) Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 On Wed, 2026-06-17 at 11:59 +0200, Nam Cao wrote: > Gabriele Monaco writes: > > This function used to validate things we are no longer validating, > > now it's > > alright to create a model where a clock is never reset, which > > doesn't fully > > make sense. Should we add that check somewhere else? >=20 > Theory does not require clock reset, right? Yeah, I don't see it explicitly mandated in the theory, but the description (from the sources) states: The value of a clock thus denotes the amount of time that has been =20 elapsed since its last reset But it also says (emphasis added by me): Clocks /can/ be reset to zero after which they start increasing ... Nowhere it says clocks /must/ be reset, their value simply won't make sense (according to the definition). Now in our implementation we may have some automatic reset when the monitor starts (I'm planning that to avoid invalid states), which could make explicit resets superfluous in some cases. Let's leave that to the user for now and skip this check. Thanks, Gabriele > This is not some sort of > hidden issue that trips up unsuspecting people. It is obvious from > the > model that the clock is never reset. So I think it's fine to allow > people to do that, maybe there will be an actual useful model without > clock reset, you never know. >=20 > The self.env_types check is enforced by the grammar. We do lose the > self.env_types check, but that is likely redundant anyway because we > have this: >=20 > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 for transition in self.transit= ions: > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 [...] > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 if tra= nsition.reset: > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 envs.append(transition.reset.env) > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 self.env_stored.add(transition.reset.env) >=20 > so it is clear that all envs that are reset do have a storage. >=20 > That said, I am fine with keeping these sanity checks, if you are > paranoid. >=20 > Nam