Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 2, bâtiment C JEUDI 28 juillet, 10h30 ------------- Adrien Guatto ------------- ============================== The Lazy Task Creation Machine ============================== Runtime systems are key to modern parallel programming practice. Their goal is to map the large amount of logical parallelism exposed by portable parallel software to the relatively low amount of physical parallelism offered by mainstream hardware. Doing so requires a combination of load balancing, to maximize the utilization of physical processors, and granularity control, to avoid the overheads associated with the creation of many small tasks. Lazy Task Creation is a granularity control policy according to which one defers the creation of physical parallelism until enough sequential work has been carried out. This idea, originally put forward by Mohr et al. for use in the Mul-T parallel Scheme system, has since been implemented in various production runtimes, including those of Cilk and Intel Thread Building Blocks. However, Lazy Task Creation has never been formalized up to now, making it difficult to study its correctness or efficiency independently from concrete implementations. In this talk, I will present a formalization of lazy task creation. We start from a straightforward sequential CEK-style abstract machine for an applied lambda-calculus with pairs. Then, we describe lazy task creation as a big-step semantics which extracts parallelism from evaluation contexts in a lazy manner. This semantics defines not only the result of each execution but also its cost, expressed in terms of work and span. We use these costs to prove analytic bounds on the overhead of lazy task creation compared to the fully sequential and fully parallel implementations. The bounds imply that, if properly set up, lazy task creation indeed amortizes scheduling overheads while preserving parallelism, independently of any specific choice of scheduling policy. This work is done in collaboration with Umut Acar, Arthur Charguéraud, Filip Sieczkowski, and Mike Rainey.