Formalisation of FunLoft

Frédéric Boussinot 1 Frederic Dabrowski 2
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We formalise a thread-based concurrent language which makes resource control possible. Concurrency is based on a two-level model: threads are executed cooperatively when linked to a scheduler, and unlinked threads and schedulers are executed preemptively, under the control of the OS. We present a type and effect system to enforce a logical separation of the memory which ensures that (1) when running in preemptive mode, threads do not interfere with other threads; (2) threads linked to a scheduler do not interfere with threads linked to another scheduler. Thus, we get a concurrency model in which well-typed programs are free from data-races. The type system also insures that well-typed programs are bounded in memory and in their use of the CPU. Detection of termination of recursive functions and stratification of references in memory are techniques used to get these properties.
Type de document :
Pré-publication, Document de travail
2007
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00183242
Contributeur : Frederic Boussinot <>
Soumis le : lundi 29 octobre 2007 - 15:57:24
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : lundi 24 septembre 2012 - 14:45:29

Fichier

fl_formal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00183242, version 1

Citation

Frédéric Boussinot, Frederic Dabrowski. Formalisation of FunLoft. 2007. 〈inria-00183242〉

Partager

Métriques

Consultations de la notice

320

Téléchargements de fichiers

184