diff options
Diffstat (limited to 'chapters/schedule.tex')
| -rw-r--r-- | chapters/schedule.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/chapters/schedule.tex b/chapters/schedule.tex index bf62c59..d367e4b 100644 --- a/chapters/schedule.tex +++ b/chapters/schedule.tex @@ -42,10 +42,10 @@ proof. Vericert to pass through \SSA, as well as GSA, and finally generate dynamic HTL (or some other similar hardware language). During my visit at Inria Rennes, I worked with Sandrine Blazy and Delphine Demange to extend CompCertSSA~\cite[barthe14_formal_verif_ssa_based_middl_end_compc] with -\GSA~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global -optimisations of \SSA\ code, but it should also allow for a more straightforward translation to -hardware as the GSA code can just be viewed as a \DFG. Instead of working on modulo scheduling, it -could therefore be interesting to work on a formally verified dynamic scheduling translation. +\GSA~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global optimisations of +\SSA\ code, but it should also allow for a more straightforward translation to hardware as the GSA +code can just be viewed as a \DFG. Instead of working on modulo scheduling, it could therefore be +interesting to work on a formally verified dynamic scheduling translation. \startplacemarginfigure[ title={Gantt chart describing the future plan for 2022 and 2023. The main funding runs out |