User Tools

Site Tools


Stuff to do

Memory Models and Scheduling (Oct 6, 2009)
  • orthogonal issues, but closely related
  • Need to tie together 10tldi and 09concurrency
  • Hypothesis: if →pr then →cr, where →pr is preemptive/relaxed_mm execution and →cr is cooperative/relaxed_mm execution
  • Ideally, if →pr then →c : a well-formed program, even w/ races, still executes according to s.c. and cooperative annotations.
  • Some races are impossible due to scheduling;

  • Some races are related to scheduling.

  • Relationship between various semantics

Yield checking in RR
Yield inference in RR
Other Stuff
  • Eclipse - infer lots of yield annots & sc-races
  • “sequentially-consistent race”; JMM; AME
    • Same syntax, different semantics: good code under AME is good under JMM?
    • a race is “OK”; why? Is it bad scheduling, or bad memory model?
    •  (t1)           (t2)
      x = 0
                  while(x==0) //sc
      x = 1 //sc
    •  (t1)           (t2)
      x = 1       rd x // sc with both yields, nsc if only one
  • yield(x, y.f, z.*, a[*]): expected read set/write set
  • relation of yield's read/write set to communication channels
  • SC(P) ⊆ HB(P): trivial
  • HB(P) ⊆ SC(P): ?
Type System
  • type system for Java or for IMP
  • similar to Types for Atomicity paper (PLDI03) or TLDI03
  • deadlocking issue?
  • soundness proof?
  • implementation? (5KLOC)
projects/yieldidiom.txt · Last modified: 2009/10/06 20:56 by jaeheon