1 minute read

Cost semantics is to discuss: How long do programs run (abstractly)?

The idea of cost semantics for parallelism is that we have the concrete ability to compute simultaneously.

Simple Example of Product TypesPermalink

For sequential computation we have:

e1seqe1(e1,e2)seq(e1,e2) e1 val;e2seqe2(e1,e2)seq(e1,e2)

For parallel computation we have:

e1pare1;e2pare2(e1,e2)par(e1,e2)

Deterministic ParallelismPermalink

eseqv iff ev iff eparv

It means that we are getting the same answer, just (potentially) faster.

Given a closed program e, we can count the number of seq (or w “work”) and the number of par (or s “span”)

Cost SemanticsPermalink

We annotate ew,sv to keep tract of work and span.

e1w1,s1v1;e2w2,s2v2e1,e2)w1+w2,max(s1,s2)(v1,v2) e1w1,s1(v1,v2);[v1/x][v2/y]e2w2,s2vlet(x,y)=e1 in e2w1+w2+1,s1+s2+1v If ew,sv then ewseqv and esparv If ewseqv thens ew,sv If esparv thenw ew,sv If ew,sv and ew,sv then w=w,s=s

Brent’s PrinciplePermalink

In general, it is a principle about how work and span predict evaluation in some machine.

For example, for a machine that has p processors:

If ew,sv then e can be run to v in time O(max(wp,s))

Machine with StatesPermalink

Local TransitionsPermalink

γΣa1,...,an{a1s1...ansn}

a’s are names for the tasks, and

s:=e|join[a](x.e)|join[a1,a2](x,y.e)

Where join[a](x.e) means to “wait for task a to complete, and then plug it’s value in for x”, and join[a1,a2](x,y.e) means to wait for two tasks.

Suppose one of e1,e2 is not val, we have the following, which is also called fork:

γa{a(e1,e2)}γa,a1,a2{a1e1,a2e2,ajoin[a1,a2](x,y.(x,y))}

And we have join:

γa1,a2,a{a1v1,a2v2,ajoin[a1,a2](x1,x2.e)}γa{a[v1/x2][v2/x2]e}

Similarly for let:

γa{alet(x,y)=e1 in e2}γa1,a{a1e1,ajoin[a1](z.let(x,y) in e2)}

Global TransitionsPermalink

  • Select 1kp tasks to make local transitions
  • Step locally
  • Each creates or garbage collectos processes (global synchronization by αrenaming)

SchedulingPermalink

How to we “Select 1kp tasks to make local transitions” e.g DFS, BFS

Comments