BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:3e55db96-1003-4153-8110-e79a07a8da16
X-WR-CALNAME:[M2F] Parosh Adbulla
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20261025T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:3e55db96-1003-4153-8110-e79a07a8da16
DTSTAMP:20260407T074546Z
CLASS:PUBLIC
DESCRIPTION:Verifying Liveness Properties under Weak Memory Models \n\nI wi
 ll discuss verifying liveness properties for concurrent programs running o
 n\nweak memory models. To that end\, I will introduce the notion of\nMemor
 y-Boundness-Fairness (MBF) that precludes demonic memory updates that make
 \nmost liveness properties trivially unsatisfiable. MBF implies the existe
 nce of\nan (unknown) bound on the number of messages in transient in the m
 emory system. \nIn the case of the classical TSO semantics\, MBF says that
  the store buffers are\nbounded in size\, although the bound is not known.
  MBF is motivated by practical\nlimitations on the system\, such as the ph
 ysical size of the underlying hardware. \nFurthermore\, we show that MBF m
 akes liveness properties amenable to algorithmic\nverification. \n\nTo dev
 elop algorithms for checking liveness conditions under MBF\, we consider a
 n\nalternative fairness condition\, namely probabilistic fairness\, and sh
 ow that MBF\ncoincides with probabilistic fairness in liveness verificatio
 n. We exploit this\nconnection to reduce the liveness checking problem (re
 peated state reachability)\nto the safety checking problem (simple state r
 eachability). We show this is a\ngeneral phenomenon by developing a unifor
 m framework that is the formal\nfoundation of our fairness definition and 
 can be instantiated to a broad\nlandscape of memory models. These models i
 nclude SC\, TSO\, PSO\, (Strong/Weak)\nRelease-Acquire\, Strong Coherence\
 , Causal Consistency\, FIFO Consistency\, and\nRMO. \n\n\nImport automatiq
 ue depuis https://framagenda.org/remote.php/dav/public-calendars/D3yqF7nwy
 s9amfyY?export par sync_icals_to_drupal.py pour M2F
DTSTART;TZID=Europe/Paris:20241129T110000
DTEND;TZID=Europe/Paris:20241129T120000
LOCATION:sale 178
SEQUENCE:0
SUMMARY:[M2F] Parosh Adbulla
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
