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


214

in

215

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

216


217


218

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

219

let dependence_graph mems non_inputs n =

220

eq_var_cpt := 0;

221

instance_var_cpt := 0;

222

let g = new_graph (), new_graph () in

223

(* Basic dependencies *)

224

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

225

g

226


227

end

228


229

module NodeDep = struct

230


231

module ExprModule =

232

struct

233

type t = expr

234

let compare = compare

235

let hash n = Hashtbl.hash n

236

let equal n1 n2 = n1 = n2

237

end

238


239

module ESet = Set.Make(ExprModule)

240


241

let rec get_expr_calls prednode expr =

242

match expr.expr_desc with

243

 Expr_const _

244

 Expr_ident _ > ESet.empty

245

 Expr_access (e, _)

246

 Expr_power (e, _) > get_expr_calls prednode e

247

 Expr_array t

248

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

249

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

250

 Expr_fby (e1,e2)

251

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

252

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

253

 Expr_pre e

254

 Expr_when (e,_,_) > get_expr_calls prednode e

255

 Expr_appl (id,e, _) >

256

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

257

then ESet.add expr (get_expr_calls prednode e)

258

else (get_expr_calls prednode e)

259


260

let get_callee expr =

261

match expr.expr_desc with

262

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

263

 _ > None

264


265

let get_calls prednode eqs =

266

let deps =

267

List.fold_left

268

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

269

ESet.empty

270

eqs in

271

ESet.elements deps

272


273

let dependence_graph prog =

274

let g = new_graph () in

275

let g = List.fold_right

276

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

277

match td.top_decl_desc with

278

 Node nd >

279

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

280

let accu = add_vertices [nd.node_id] accu in

281

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

282

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

283

add_edges [nd.node_id] deps accu

284

 _ > assert false (* should not happen *)

285


286

) prog g in

287

g

288


289

let rec filter_static_inputs inputs args =

290

match inputs, args with

291

 [] , [] > []

292

 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

293

 _ > assert false

294


295

let compute_generic_calls prog =

296

List.iter

297

(fun td >

298

match td.top_decl_desc with

299

 Node nd >

300

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

301

nd.node_gencalls < get_calls prednode nd.node_eqs

302

 _ > ()

303


304

) prog

305


306

end

307


308

module CycleDetection = struct

309


310

(*  Look for cycles in a dependency graph *)

311

module Cycles = Graph.Components.Make (IdentDepGraph)

312


313

let mk_copy_var n id =

314

mk_new_name (node_vars n) id

315


316

let mk_copy_eq n var =

317

let var_decl = node_var var n in

318

let cp_var = mk_copy_var n var in

319

let expr =

320

{ expr_tag = Utils.new_tag ();

321

expr_desc = Expr_ident var;

322

expr_type = var_decl.var_type;

323

expr_clock = var_decl.var_clock;

324

expr_delay = Delay.new_var ();

325

expr_annot = None;

326

expr_loc = var_decl.var_loc } in

327

{ var_decl with var_id = cp_var },

328

mkeq var_decl.var_loc ([cp_var], expr)

329


330

let wrong_partition g partition =

331

match partition with

332

 [id] > IdentDepGraph.mem_edge g id id

333

 _::_::_ > true

334

 [] > assert false

335


336

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

337

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

338

let check_cycles g =

339

let scc_l = Cycles.scc_list g in

340

List.iter (fun partition >

341

if wrong_partition g partition then

342

raise (Cycle partition)

343

else ()

344

) scc_l

345


346

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

347

let copy_partition g partition =

348

let copy_g = IdentDepGraph.create () in

349

IdentDepGraph.iter_edges

350

(fun src tgt >

351

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

352

then IdentDepGraph.add_edge copy_g src tgt)

353

g

354


355


356

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

357

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

358

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

359

let break_cycle head cp_head g =

360

let succs = IdentDepGraph.succ g head in

361

IdentDepGraph.add_edge g head cp_head;

362

List.iter

363

(fun s >

364

IdentDepGraph.remove_edge g head s;

365

IdentDepGraph.add_edge g s cp_head)

366

succs

367


368

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

369

belonging in node [node]. Returns:

370

 a list of new auxiliary variable declarations

371

 a list of new equations

372

 a modified acyclic version of [g]

373

*)

374

let break_cycles node mems g =

375

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

376

let rec break vdecls mem_eqs g =

377

let scc_l = Cycles.scc_list g in

378

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

379

match wrong with

380

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

381

 [head]::_ >

382

begin

383

IdentDepGraph.remove_edge g head head;

384

break vdecls mem_eqs g

385

end

386

 (head::part)::_ >

387

begin

388

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

389

let pvar v = List.mem v part in

390

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

391

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

392

break_cycle head vdecl_cp_head.var_id g;

393

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

394

end

395

 _ > assert false

396

in break [] mem_eqs g

397


398

end

399


400

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

401

module Disjunction =

402

struct

403

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

404

maybe removing shorter branches *)

405

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

406


407

let rec add_vdecl map vdecls =

408

match vdecls with

409

 [] > ()

410

 vdecl :: q > begin

411

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);

412

add_vdecl map q

413

end

414


415

let clock_disjoint_map vdecls =

416

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

417

let map = Hashtbl.create 23 in

418

begin

419

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

420

map

421

end

422


423

let pp_disjoint_map fmt map =

424

begin

425

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

426

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

427

Format.fprintf fmt "}@."

428

end

429

end

430


431

let pp_dep_graph fmt g =

432

begin

433

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

434

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

435

Format.fprintf fmt "}@."

436

end

437


438

let pp_error fmt trace =

439

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

440

(fprintf_list ~sep:">" pp_print_string) trace

441


442

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

443

let merge_with g1 g2 =

444

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

445

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

446


447

let global_dependency node =

448

let mems = ExprDep.node_memory_variables node in

449

let non_inputs = ExprDep.node_non_input_variables node in

450

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

451

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

452

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

453

CycleDetection.check_cycles g_non_mems;

454

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

455

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

456

merge_with g_non_mems g_mems';

457

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

458

g_non_mems

459


460


461

(* Local Variables: *)

462

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

463

(* End: *)
