From f4cdf7ca9a1fdcca413157df19753f388a5a224e Mon Sep 17 00:00:00 2001 From: Linus Torvalds Date: Wed, 19 Aug 2026 10:09:22 -0700 Subject: Merge tag 'media/v7.3-1' of git://git.kernel.org/pub/scm/linux/kernel/git/mchehab/linux-media Pull media updates from Mauro Carvalho Chehab: - v4l2-core: added ISP statistics support and per-block validation - v4l2-core: Allow unknown HDR10 white point and luminance - New camera sensors: Sony IMX678 and IMX471m, Himax HM1092 IR sensor - New codec: Milos: VPU v2.0 codec support - isp driver: gained support for Dreamchip RPPX1 ISP framework - vsp1 driver: gained support for RZ/T2H and RZ/N2H - Novalake driver: gained CVS support for new NVL hardware - dvb-core: fix feed leak on failed DMX_ADD_PID - several driver fixes, cleanups and minor improvements * tag 'media/v7.3-1' of git://git.kernel.org/pub/scm/linux/kernel/git/mchehab/linux-media: (308 commits) media: ipu-bridge: check all DMI entries when overriding sensor rotation media: v4l2-async: avoid deleting unlinked ASC entry on link error media: rzg2l-cru: Align bytesperline to hardware DMA stride requirement media: intel/ipu6: fix async notifier cleanup leak on parse error media: staging/ipu7: fix async notifier UAF on probe error path media: amd: isp4: fix self-deadlock in isp4sd_pwron_and_init() error path media: amd: isp4: release partial allocations in isp4if_alloc_fw_gpumem() media: rcar-isp: Fix VSPX reference leaks media: rcar-isp: Release ISPCORE resources media: i2c: imx415: Release runtime PM reference on VBLANK error media: i2c: imx415: Return test pattern write errors media: renesas: vsp1: Declare index variables in for loop statement media: renesas: vsp1: Make reset control optional to support platforms without a reset line media: dt-bindings: media: renesas,vsp1: Document RZ/T2H and RZ/N2H SoCs media: dt-bindings: media: renesas,fcp: Document RZ/T2H and RZ/N2H SoCs media: nxp: imx8-isi: Add additional 32-bit RGB format support media: nxp: imx8-isi: Add 16-bit raw Bayer format support media: nxp: imx8-isi: Implement per-stream reference counting for multiplexed streams media: nxp: imx8-isi: Use BIT_ULL() for 64-bit stream masks media: nxp: imx8-isi: Correct color map between V4L2 and ISI ... --- tools/memory-model/lock.cat | 157 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 157 insertions(+) create mode 100644 tools/memory-model/lock.cat (limited to 'tools/memory-model/lock.cat') diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat new file mode 100644 index 000000000..03c12efed --- /dev/null +++ b/tools/memory-model/lock.cat @@ -0,0 +1,157 @@ +// SPDX-License-Identifier: GPL-2.0+ +(* + * Copyright (C) 2016 Luc Maranget for Inria + * Copyright (C) 2017 Alan Stern + *) + +(* + * Generate coherence orders and handle lock operations + *) + +include "cross.cat" + +(* + * The lock-related events generated by herd7 are as follows: + * + * LKR Lock-Read: the read part of a spin_lock() or successful + * spin_trylock() read-modify-write event pair + * LKW Lock-Write: the write part of a spin_lock() or successful + * spin_trylock() RMW event pair + * UL Unlock: a spin_unlock() event + * LF Lock-Fail: a failed spin_trylock() event + * RL Read-Locked: a spin_is_locked() event which returns True + * RU Read-Unlocked: a spin_is_locked() event which returns False + * + * LKR and LKW events always come paired, like all RMW event sequences. + * + * LKR, LF, RL, and RU are read events; LKR has Acquire ordering. + * LKW and UL are write events; UL has Release ordering. + * LKW, LF, RL, and RU have no ordering properties. + *) + +(* Backward compatibility *) +let RL = try RL with emptyset +let RU = try RU with emptyset + +(* Treat RL as a kind of LF: a read with no ordering properties *) +let LF = LF | RL + +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *) +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses + +(* Link Lock-Reads to their RMW-partner Lock-Writes *) +let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) +let rmw = rmw | lk-rmw + +(* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *) +flag ~empty LKW \ range(lk-rmw) as unpaired-LKW +flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR + +(* + * An LKR must always see an unlocked value; spin_lock() calls nested + * inside a critical section (for the same lock) always deadlock. + *) +empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest + +(* + * In the same way, spin_is_locked() inside a critical section must always + * return True (no RU events can be in a critical section for the same lock). + *) +empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked + +(* The final value of a spinlock should not be tested *) +flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final + +(* + * Put lock operations in their appropriate classes, but leave UL out of W + * until after the co relation has been generated. + *) +let R = R | LKR | LF | RU +let W = W | LKW + +let Release = Release | UL +let Acquire = Acquire | LKR + +(* Match LKW events to their corresponding UL events *) +let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc) + +flag ~empty UL \ range(critical) as unmatched-unlock + +(* Allow up to one unmatched LKW per location; more must deadlock *) +let UNMATCHED-LKW = LKW \ domain(critical) +empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks + +(* rfi for LF events: link each LKW to the LF events in its critical section *) +let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc) + +(* Utility macro to convert a single pair to a single-edge relation *) +let pair-to-relation p = p ++ 0 + +(* + * If a given LF event e is outside a critical section, it cannot read + * internally but it may read from an LKW event in another thread. + * Compute the relation containing these possible edges. + *) +let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext + +(* Compute set of sets of possible rfe edges for LF events *) +let all-possible-rfe-lf = + (* + * Convert the possible-rfe-noncrit-lf relation for e + * to a set of single edges + *) + let set-of-singleton-rfe-lf e = + map pair-to-relation (possible-rfe-noncrit-lf e) + (* Do this for each LF event e that isn't in rfi-lf *) + in map set-of-singleton-rfe-lf (LF \ range(rfi-lf)) + +(* Generate all rf relations for LF events *) +with rfe-lf from cross(all-possible-rfe-lf) +let rf-lf = rfe-lf | rfi-lf + +(* + * A given RU event e may read internally from the last po-previous UL, + * or it may read from a UL event in another thread or the initial write. + * Compute the relation containing these possible edges. + *) +let possible-rf-ru e = (((UL * {e}) & po-loc) \ + ([UL] ; po-loc ; [UL] ; po-loc)) | + (((UL | IW) * {e}) & loc & ext) + +(* Compute set of sets of possible rf edges for RU events *) +let all-possible-rf-ru = + (* Convert the possible-rf-ru relation for e to a set of single edges *) + let set-of-singleton-rf-ru e = + map pair-to-relation (possible-rf-ru e) + (* Do this for each RU event e *) + in map set-of-singleton-rf-ru RU + +(* Generate all rf relations for RU events *) +with rf-ru from cross(all-possible-rf-ru) + +(* Final rf relation *) +let rf = rf | rf-lf | rf-ru + +(* Generate all co relations, including LKW events but not UL *) +let co0 = co0 | ([IW] ; loc ; [LKW]) | + (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW]) +include "cos-opt.cat" +let W = W | UL +let M = R | W + +(* Merge UL events into co *) +let co = (co | critical | (critical^-1 ; co))+ +let coe = co & ext +let coi = co & int + +(* Merge LKR events into rf *) +let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1) +let rfe = rf & ext +let rfi = rf & int + +let fr = rf^-1 ; co +let fre = fr & ext +let fri = fr & int + +show co,rf,fr -- cgit v1.3.1