1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE

4

*

5

* This file is part of Prelude

6

*

7

* Prelude is free software; you can redistribute it and/or

8

* modify it under the terms of the GNU Lesser General Public License

9

* as published by the Free Software Foundation ; either version 2 of

10

* the License, or (at your option) any later version.

11

*

12

* Prelude is distributed in the hope that it will be useful, but

13

* WITHOUT ANY WARRANTY ; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

15

* Lesser General Public License for more details.

16

*

17

* You should have received a copy of the GNU Lesser General Public

18

* License along with this program ; if not, write to the Free Software

19

* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307

20

* USA

21

* *)

22


23


24

(** Simple modular syntactic causality analysis. Can reject correct

25

programs, especially if the program is not flattened first. *)

26

open Utils

27

open LustreSpec

28

open Corelang

29

open Graph

30

open Format

31


32

exception Cycle of ident list

33


34

module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)

35


36

(*module IdentDepGraphUtil = Oper.P(IdentDepGraph)*)

37


38

(* Dependency of mem variables on mem variables is cut off

39

by duplication of some mem vars into local node vars.

40

Thus, cylic dependency errors may only arise between nomem vars.

41


42

no_mem' = combinational(no_mem, mem);

43

=> (mem > no_mem' > no_mem)

44


45

mem' = pre(no_mem, mem);

46

=> (mem' > no_mem), (mem > mem')

47


48

Global roadmap:

49

 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem)

50

 check cycles in g (a cycle means a dependency error)

51

 break cycles in g' (it's legal !):

52

 check cycles in g'

53

 if any, introduce aux var to break cycle, then start afresh

54

 insert g' into g

55

 return g

56

*)

57


58

(* Tests whether [v] is a root of graph [g], i.e. a source *)

59

let is_graph_root v g =

60

IdentDepGraph.in_degree g v = 0

61


62

(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)

63

let graph_roots g =

64

IdentDepGraph.fold_vertex

65

(fun v roots > if is_graph_root v g then v::roots else roots)

66

g []

67


68

let add_edges src tgt g =

69

(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*)

70

List.iter

71

(fun s >

72

List.iter

73

(fun t > IdentDepGraph.add_edge g s t)

74

tgt)

75

src;

76

g

77


78

let add_vertices vtc g =

79

(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*)

80

List.iter (fun v > IdentDepGraph.add_vertex g v) vtc;

81

g

82


83

let new_graph () =

84

IdentDepGraph.create ()

85


86

module ExprDep = struct

87


88

let eq_var_cpt = ref 0

89


90

let instance_var_cpt = ref 0

91


92

let mk_eq_var id =

93

incr eq_var_cpt; sprintf "#%s_%d" id !eq_var_cpt

94


95

let mk_instance_var id =

96

incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt

97


98

let is_eq_var v = v.[0] = '#'

99


100

let is_instance_var v = v.[0] = '!'

101


102

let is_ghost_var v = is_instance_var v  is_eq_var v

103


104

let eq_memory_variables mems eq =

105

let rec match_mem lhs rhs mems =

106

match rhs.expr_desc with

107

 Expr_fby _

108

 Expr_pre _ > List.fold_right ISet.add lhs mems

109

 Expr_tuple tl >

110

let lhs' = (transpose_list [lhs]) in

111

if List.length tl <> List.length lhs' then

112

assert false;

113

List.fold_right2 match_mem lhs' tl mems

114

 _ > mems in

115

match_mem eq.eq_lhs eq.eq_rhs mems

116


117

let node_memory_variables nd =

118

List.fold_left eq_memory_variables ISet.empty nd.node_eqs

119


120

let node_non_input_variables nd =

121

let outputs = List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs in

122

List.fold_left (fun non_inputs v > ISet.add v.var_id non_inputs) outputs nd.node_locals

123


124

(* computes the equivalence relation relating variables

125

in the same equation lhs, under the form of a table

126

of class representatives *)

127

let node_eq_equiv nd =

128

let eq_equiv = Hashtbl.create 23 in

129

List.iter (fun eq >

130

let first = List.hd eq.eq_lhs in

131

List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs

132

)

133

nd.node_eqs;

134

eq_equiv

135


136

(* Create a tuple of right dimension, according to [expr] type, *)

137

(* filled with variable [v] *)

138

let adjust_tuple v expr =

139

match expr.expr_type.Types.tdesc with

140

 Types.Ttuple tl > duplicate v (List.length tl)

141

 _ > [v]

142


143


144

(* Add dependencies from lhs to rhs in [g, g'], *)

145

(* nomem/nomem and mem/nomem in g *)

146

(* mem/mem in g' *)

147

(* excluding all/[inputs] *)

148

let add_eq_dependencies mems non_inputs eq (g, g') =

149

let add_var lhs_is_mem lhs x (g, g') =

150

if is_instance_var x  ISet.mem x non_inputs then

151

match (lhs_is_mem, ISet.mem x mems) with

152

 (false, true ) > (add_edges [x] lhs g, g' )

153

 (false, false) > (add_edges lhs [x] g, g' )

154

 (true , false) > (add_edges lhs [x] g, g' )

155

 (true , true ) > (g , add_edges [x] lhs g')

156

else (g, g') in

157

(* Add dependencies from [lhs] to rhs clock [ck]. *)

158

let rec add_clock lhs_is_mem lhs ck g =

159

(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)

160

match (Clocks.repr ck).Clocks.cdesc with

161

 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)

162

 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g

163

 _ > g

164

in

165


166


167

let rec add_dep lhs_is_mem lhs rhs g =

168


169

(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *)

170

(* i.e every input is connected to every output, through a ghost var *)

171

let mashup_appl_dependencies f e g =

172

let f_var = mk_instance_var (sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in

173

List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)

174

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

175

in

176

match rhs.expr_desc with

177

 Expr_const _ > g

178

 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g)

179

 Expr_pre e > add_dep true lhs e g

180

 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)

181

 Expr_access (e1, _)

182

 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g

183

 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g

184

 Expr_tuple t >

185

if List.length t <> List.length lhs then (

186

match lhs with

187

 [l] > List.fold_right (fun r > add_dep lhs_is_mem [l] r) t g

188

 _ >

189

Format.eprintf "Incompatible tuple assign: %a (%i) vs %a (%i)@.@?"

190

(Utils.fprintf_list ~sep:"," (Format.pp_print_string)) lhs

191

(List.length lhs)

192

Printers.pp_expr rhs

193

(List.length t)

194

;

195

assert false

196

)

197

else

198

List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g

199

 Expr_merge (c, hl) > add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) > add_dep lhs_is_mem lhs h) hl g)

200

 Expr_ite (c, t, e) > add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))

201

 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)

202

 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)

203

 Expr_appl (f, e, None) >

204

if Basic_library.is_internal_fun f

205

(* tuple componentwise dependency for internal operators *)

206

then

207

List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g

208

(* mashed up dependency for userdefined operators *)

209

else

210

mashup_appl_dependencies f e g

211

 Expr_appl (f, e, Some (r, _)) >

212

mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)

213

 Expr_uclock (e, _)

214

 Expr_dclock (e, _)

215

 Expr_phclock (e, _) > add_dep lhs_is_mem lhs e g

216

in

217

add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g')

218


219


220

(* Returns the dependence graph for node [n] *)

221

let dependence_graph mems non_inputs n =

222

eq_var_cpt := 0;

223

instance_var_cpt := 0;

224

let g = new_graph (), new_graph () in

225

(* Basic dependencies *)

226

let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in

227

g

228


229

end

230


231

module NodeDep = struct

232


233

module ExprModule =

234

struct

235

type t = expr

236

let compare = compare

237

let hash n = Hashtbl.hash n

238

let equal n1 n2 = n1 = n2

239

end

240


241

module ESet = Set.Make(ExprModule)

242


243

let rec get_expr_calls prednode expr =

244

match expr.expr_desc with

245

 Expr_const _

246

 Expr_ident _ > ESet.empty

247

 Expr_access (e, _)

248

 Expr_power (e, _) > get_expr_calls prednode e

249

 Expr_array t

250

 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty

251

 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty

252

 Expr_fby (e1,e2)

253

 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)

254

 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))

255

 Expr_pre e

256

 Expr_when (e,_,_)

257

 Expr_uclock (e,_)

258

 Expr_dclock (e,_)

259

 Expr_phclock (e,_) > get_expr_calls prednode e

260

 Expr_appl (id,e, _) >

261

if not (Basic_library.is_internal_fun id) && prednode id

262

then ESet.add expr (get_expr_calls prednode e)

263

else (get_expr_calls prednode e)

264


265

let get_callee expr =

266

match expr.expr_desc with

267

 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args)

268

 _ > None

269


270

let get_calls prednode eqs =

271

let deps =

272

List.fold_left

273

(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs))

274

ESet.empty

275

eqs in

276

ESet.elements deps

277


278

let dependence_graph prog =

279

let g = new_graph () in

280

let g = List.fold_right

281

(fun td accu > (* for each node we add its dependencies *)

282

match td.top_decl_desc with

283

 Node nd >

284

(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)

285

let accu = add_vertices [nd.node_id] accu in

286

let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) nd.node_eqs) in

287

(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)

288

add_edges [nd.node_id] deps accu

289

 _ > assert false (* should not happen *)

290


291

) prog g in

292

g

293


294

let rec filter_static_inputs inputs args =

295

match inputs, args with

296

 [] , [] > []

297

 v::vq, a::aq > if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq

298

 _ > assert false

299


300

let compute_generic_calls prog =

301

List.iter

302

(fun td >

303

match td.top_decl_desc with

304

 Node nd >

305

let prednode n = is_generic_node (Hashtbl.find node_table n) in

306

nd.node_gencalls < get_calls prednode nd.node_eqs

307

 _ > ()

308


309

) prog

310


311

end

312


313

module CycleDetection = struct

314


315

(*  Look for cycles in a dependency graph *)

316

module Cycles = Graph.Components.Make (IdentDepGraph)

317


318

let mk_copy_var n id =

319

mk_new_name (node_vars n) id

320


321

let mk_copy_eq n var =

322

let var_decl = node_var var n in

323

let cp_var = mk_copy_var n var in

324

let expr =

325

{ expr_tag = Utils.new_tag ();

326

expr_desc = Expr_ident var;

327

expr_type = var_decl.var_type;

328

expr_clock = var_decl.var_clock;

329

expr_delay = Delay.new_var ();

330

expr_annot = None;

331

expr_loc = var_decl.var_loc } in

332

{ var_decl with var_id = cp_var },

333

mkeq var_decl.var_loc ([cp_var], expr)

334


335

let wrong_partition g partition =

336

match partition with

337

 [id] > IdentDepGraph.mem_edge g id id

338

 _::_::_ > true

339

 [] > assert false

340


341

(* Checks that the dependency graph [g] does not contain a cycle. Raises

342

[Cycle partition] if the succession of dependencies [partition] forms a cycle *)

343

let check_cycles g =

344

let scc_l = Cycles.scc_list g in

345

List.iter (fun partition >

346

if wrong_partition g partition then

347

raise (Cycle partition)

348

else ()

349

) scc_l

350


351

(* Creates the subgraph of [g] restricted to vertices and edges in partition *)

352

let copy_partition g partition =

353

let copy_g = IdentDepGraph.create () in

354

IdentDepGraph.iter_edges

355

(fun src tgt >

356

if List.mem src partition && List.mem tgt partition

357

then IdentDepGraph.add_edge copy_g src tgt)

358

g

359


360


361

(* Breaks dependency cycles in a graph [g] by inserting aux variables.

362

[head] is a head of a nontrivial scc of [g].

363

In Lustre, this is legal only for mem/mem cycles *)

364

let break_cycle head cp_head g =

365

let succs = IdentDepGraph.succ g head in

366

IdentDepGraph.add_edge g head cp_head;

367

List.iter

368

(fun s >

369

IdentDepGraph.remove_edge g head s;

370

IdentDepGraph.add_edge g s cp_head)

371

succs

372


373

(* Breaks cycles of the dependency graph [g] of memory variables [mems]

374

belonging in node [node]. Returns:

375

 a list of new auxiliary variable declarations

376

 a list of new equations

377

 a modified acyclic version of [g]

378

*)

379

let break_cycles node mems g =

380

let (mem_eqs, non_mem_eqs) = List.partition (fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs) node.node_eqs in

381

let rec break vdecls mem_eqs g =

382

let scc_l = Cycles.scc_list g in

383

let wrong = List.filter (wrong_partition g) scc_l in

384

match wrong with

385

 [] > (vdecls, non_mem_eqs@mem_eqs, g)

386

 [head]::_ >

387

begin

388

IdentDepGraph.remove_edge g head head;

389

break vdecls mem_eqs g

390

end

391

 (head::part)::_ >

392

begin

393

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

394

let pvar v = List.mem v part in

395

let fvar v = if v = head then vdecl_cp_head.var_id else v in

396

let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in

397

break_cycle head vdecl_cp_head.var_id g;

398

break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g

399

end

400

 _ > assert false

401

in break [] mem_eqs g

402


403

end

404


405

(* Module used to compute static disjunction of variables based upon their clocks. *)

406

module Disjunction =

407

struct

408

(* map: var > list of disjoint vars, sorted in increasing branch length,

409

maybe removing shorter branches *)

410

type clock_map = (ident, ident list) Hashtbl.t

411


412

let rec add_vdecl map vdecls =

413

match vdecls with

414

 [] > ()

415

 vdecl :: q > begin

416

Hashtbl.add map vdecl.var_id (List.fold_left (fun r v > if Clocks.disjoint v.var_clock vdecl.var_clock then v.var_id::r else r) [] q);

417

add_vdecl map q

418

end

419


420

let clock_disjoint_map vdecls =

421

let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in

422

let map = Hashtbl.create 23 in

423

begin

424

add_vdecl map (List.sort (fun v1 v2 > compare (root_branch v1) (root_branch v2)) vdecls);

425

map

426

end

427


428

let pp_disjoint_map fmt map =

429

begin

430

Format.fprintf fmt "{ /* disjoint map */@.";

431

Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;

432

Format.fprintf fmt "}@."

433

end

434

end

435


436

let pp_dep_graph fmt g =

437

begin

438

Format.fprintf fmt "{ /* graph */@.";

439

IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g;

440

Format.fprintf fmt "}@."

441

end

442


443

let pp_error fmt trace =

444

fprintf fmt "@.Causality error, cyclic data dependencies: %a@."

445

(fprintf_list ~sep:">" pp_print_string) trace

446


447

(* Merges elements of graph [g2] into graph [g1] *)

448

let merge_with g1 g2 =

449

IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2;

450

IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2

451


452

let global_dependency node =

453

let mems = ExprDep.node_memory_variables node in

454

let non_inputs = ExprDep.node_non_input_variables node in

455

let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in

456

(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;

457

Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)

458

CycleDetection.check_cycles g_non_mems;

459

let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in

460

(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)

461

merge_with g_non_mems g_mems';

462

{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals },

463

g_non_mems

464


465


466

(* Local Variables: *)

467

(* compilecommand:"make C .." *)

468

(* End: *)
