From nobody Thu Sep 7 06:45:19 2023 X-Original-To: hackers@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4Rh8rK5vh2z4smjM for ; Thu, 7 Sep 2023 06:45:21 +0000 (UTC) (envelope-from bapt@freebsd.org) Received: from smtp.freebsd.org (smtp.freebsd.org [96.47.72.83]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "smtp.freebsd.org", Issuer "R3" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4Rh8rK391Zz4Pr5; Thu, 7 Sep 2023 06:45:21 +0000 (UTC) (envelope-from bapt@freebsd.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1694069121; 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: in-reply-to:in-reply-to:references:references; bh=C1IIzK8MS2xqG2h1uheHNTdU4S7pSSrqIlQ1SHIpSTs=; b=I+2CK0NPSH3QMae9wbTevIVkhOBOwuXFbyuJjEQQ2UbqwWrizrj4t3g70/vuunNdtHJSNY r5fLbGTbl0d+iPlDygaXDc9jfAnkgSItJ2e0ibTYZJRkL+5gfzlVEQp81t5dUTRXRTutrH hFA3r63tAiI0JJkUcvJyza1+kmtWiay1tVsuE3ctxMGo13zgnaXmamEHyn/+I2Mh1IJpGz Hb9ea3YjjZGBY1DYUchUTd6xPMo3jtIWHzmgAY21KMCzFrPMegbY1JAIVahRwSxM5XAeGP SvZNCa2h0NuB4tCgeBaFDwR2eLaot6rrqv8RsMHQx4bHwN029BiOOe+7bKOR9w== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1694069121; a=rsa-sha256; cv=none; b=OOpl2HC/Ndue+xDrTpQgQDIEZrLyyWG7kEhwlPdGwB8sN/mttES+5RvDduVjDCFJrVHe5D 5Za3QN4gJO/A0wsz2wo2nnLNY8yzVYEMpgMdTkbWFToSiM5f3wMGnWhEJsPH1IDHj7qZhp 9rQYkJMfpGnk6oBedtfdMN6fm9qJCd06nYHxwt+lMaXCMgv5ITs39TtYPQEJXfZ/7a0MEp g1W7v11P3Y6LQmL2wmb4Z0Fw8gLxGv0Axf3s+5M59d2hd7qaJ8o+ujrAyQzEiNh5Fth4Ro yoLRbGla1yT5WprOerr7Hpz3mVhUXa0efQsl6aIrzY6WyZdNuSH89Ga5026H9w== ARC-Authentication-Results: i=1; mx1.freebsd.org; none ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1694069121; 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: in-reply-to:in-reply-to:references:references; bh=C1IIzK8MS2xqG2h1uheHNTdU4S7pSSrqIlQ1SHIpSTs=; b=UnVGzCKhpsgcVYifS8ONNWlrzgtakoJTfPj2T4kARTNs0tLg6ZxhuTBY2Xahxyyeg4q4VE bE857Xv8kAZomKPZVmRnrfNsRyD0otdbUCHkdQvAY+2Edq5PW3Eho9JIqOgEQg3+GzkiJL zCkl4zxHuO4g6BURgAlNzrCxlm8+rCdk4rtvBygNWzgPWnSkO6J6m3Q/BVX7dWPVLbzWJx Zzy7Rie6qKEA2kITyArQRKOqiJDWnFBRbYcqZMGKOGxheIoQOsUSx2eQaHiPF+Z1/3Ry4c qLA/PNj7ceeFDOtug9Tn8Hn3T3qPB7u4xLPWjFKh23lB8n8aAJyoQa1MGt7zIA== Received: from aniel.nours.eu (nours.eu [176.31.115.77]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (Client did not present a certificate) (Authenticated sender: bapt) by smtp.freebsd.org (Postfix) with ESMTPSA id 4Rh8rK1ZXYz14Tr; Thu, 7 Sep 2023 06:45:21 +0000 (UTC) (envelope-from bapt@freebsd.org) Received: by aniel.nours.eu (Postfix, from userid 1001) id 3C0F9155641; Thu, 7 Sep 2023 08:45:19 +0200 (CEST) Date: Thu, 7 Sep 2023 08:45:19 +0200 From: Baptiste Daroussin To: Adriaan de Groot Cc: hackers@freebsd.org, Alexander Leidinger , c@bow.st Subject: Re: ARC model specified in spinroot/promela Message-ID: References: <5846941.Zv9zXsTiuT@beastie.bionicmutton.org> List-Id: Technical discussions relating to FreeBSD List-Archive: https://lists.freebsd.org/archives/freebsd-hackers List-Help: List-Post: List-Subscribe: List-Unsubscribe: Sender: owner-freebsd-hackers@freebsd.org MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <5846941.Zv9zXsTiuT@beastie.bionicmutton.org> On Sat, Sep 02, 2023 at 12:33:18PM +0200, Adriaan de Groot wrote: > For what it's worth, spin is available from ports (devel/spin), which I've > just adopted and updated to 6.5.2, so it is quite straightforward to get this > running on any recent FreeBSD system. > > I tested only with the ancient Peterson's mutual exclusion, which resolves > instantly. Mailing-list archives don't preserve attachments, so, Cherry, if > you could send it me directly that would be lovely. I spotted A. Mader's PLC > Controller in the SPIN documents, that is one I am familiar with, and then > realised that academic papers from the 2000s don't come with source code :( > Wrong mailing list do preserve attachemnts, since we migrated out of mailman, we stopped alterring emails if a mail is distributed via the mailing list then its integrity is preserved, if you want to get the full email later on, then you can always fallback on the .txt archive which is actually the mail in a mbox format meaning readable by any sane Mail User Agent. For example for this email: https://lists.freebsd.org/archives/freebsd-hackers/2023-September/002488.txt Bapt