*********************************************************************
* Ecole Normale Supe'rieure *
* *
* Se'minaire *
* SEMANTIQUE ET INTERPRETATION ABSTRAITE *
* P. Cousot *
* *
* Vendredi, 14h00--15h30 *
* Salle W, 4e`me e'tage, toits du DMI *
* DMI ENS 45 rue d'Ulm 75005 Paris *
*********************************************************************
*** Vendredi 3 janvier 1997 **** 14h00 *****************************
Rela^che
*** Vendredi 10 janvier 1997 **** 14h00 ****************************
Rela^che
*** Vendredi 17 janvier 1997 **** 14h00 ****************************
Rela^che (POPL'97, voir http://lix.polytechnique.fr/~radhia/popl97/)
*** Vendredi 24 janvier 1997 **** 14h00 ****************************
Continuations and threads
Expressing machine concurrency directly in advanced languages
Olin SHIVERS (MIT)
Re'sume': It is well known [Wand] that concurrency can be expressed within
languages that provide a continuation type. However, a number of misconceptions
persist regarding the relationship between threads and continuations. I
discuss the proper relationship between these two objects, and present a
model for directly expressing concurrency using continuations. The model
is designed to support systems programming, and has several novel
features: it is synchronous, preemptible, and fully virtualisable,
allowing schedulers to be written by unprivileged users that are
indistinguishable from top-level schedulers that actually control access
to the hardware resources.
Note: le se'minaire de Corrado PRIAMI (Enhanced Operational Semantics
for Concurrency) est reporte' au Vendredi 7 fe'vrier 1997.
*** Vendredi 31 janvier 1997 **** 14h00 ****************************
On deciding non-interleaving bisimulations
Pier Paolo DEGANO (Universite' de Pise, invite' ENS)
Re'sume' : We propose a new way of checking non-interleaving bisimulations
on (suitably enriched) transition systems, by reducing it to a sort of
interleaving bisimilarity check. This is done for a large variety of
non-interleaving bisimulation (roughly speaking, for all those that are
preserved by unfolding transition systems).
The basic idea is to have a linearized, incremental representation of the
non-interleaving aspects occurring in a computation of transition systems
(cf. how causality is encoded in causal trees).
This reduces the check for non-interleaving bisimilarity to a possibly
more expensive check, yet interleaving in style.
Now, suppose you wish to check that two given transition systems S1 and S2
are in a specific non-interleaving bisimulation R.
First, build a (finite) interleaving bisimulation S.
Secondly, unfold S1 and S2 until the two trees T1 and T2 you obtain
have maximal depth k, which is determined by S.
Finally, T1 R T2 if and only if S1 R S2.
The last statement implies that if a given interleaving bisimulation
(resistent to unfoldings) is decidable, then its non-interleaving versions
are such.
Joint work with Corrado Priami
*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr
WWW: http://www.ens.fr/~cousot/annonceseminaire.html
*********************************************************************