Add instruction scheduling model using SSA model
authorMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Fri, 8 May 2009 18:14:30 +0000 (14:14 -0400)
committerMathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Fri, 8 May 2009 18:14:30 +0000 (14:14 -0400)
commit03c9e0f3f9c72b36b9da30ad4b6ecb055fb6adff
tree4e43c6790c5d09477828dd2e17cee4d0b30005cc
parent6991f61a6a02d95a4275bcc90aa9bb7037a9e69e
Add instruction scheduling model using SSA model

As promised, here is a new model :-) So far the results are very good.

Basically, I model the dependencies between the instructions using a SSA
assignment. It behaves a bit like a Petri network, passing tokens
between the "instructions". When instructions have multiple dependencies
as input, they wait for all their input tokens to be ready before they
execute. It assumes we have an infinite number of registers available to
hold the variables, given this is an "abstract" architecture.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
17 files changed:
formal-model/ooomem-double-update-minimal/DEFINES [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/Makefile [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/mem.sh [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/mem.spin [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/read_order.ltl [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/read_order_no_rmb.define [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/read_order_no_wmb.define [new file with mode: 0644]
formal-model/ooomem-double-update-minimal/references.txt [new file with mode: 0644]
formal-model/ooomem-two-writes/DEFINES [new file with mode: 0644]
formal-model/ooomem-two-writes/Makefile [new file with mode: 0644]
formal-model/ooomem-two-writes/mem.sh [new file with mode: 0644]
formal-model/ooomem-two-writes/mem.spin [new file with mode: 0644]
formal-model/ooomem-two-writes/read_order.ltl [new file with mode: 0644]
formal-model/ooomem-two-writes/read_order.ltl.bkp [new file with mode: 0644]
formal-model/ooomem-two-writes/read_order_no_rmb.define [new file with mode: 0644]
formal-model/ooomem-two-writes/read_order_no_wmb.define [new file with mode: 0644]
formal-model/ooomem-two-writes/references.txt [new file with mode: 0644]
This page took 0.025162 seconds and 4 git commands to generate.