Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Session Initialize procedure should suppose Uninitialized state #788

Closed
kanigsson opened this issue Sep 30, 2021 · 0 comments · Fixed by #789
Closed

Session Initialize procedure should suppose Uninitialized state #788

kanigsson opened this issue Sep 30, 2021 · 0 comments · Fixed by #789
Assignees
@kanigsson
Labels
generator Related to generator package (SPARK code generation)
Projects
RecordFlux 0.6

Comments

@kanigsson
Copy link
Collaborator

Context and Problem Statement

The Initialize procedure of a generated session package currently does not assume that the state is uninitialized, in particular it checks if the global session variables are already allocated and frees them in that case (before reallocating them). This is an issue for the new allocator (#629), because in this scheme freeing memory is expressed by assigning the pointer back to the corresponding slot pointer. But this means that we need to know something about this pointer value that is being assigned, or else the assignment could break the memory pool.

Considered Options

O1

The best solution seems to add a precondition to Initialize that assumes the state is Uninitialized. In that case, the cleanup code could be removed. This would also add the same precondition to Run.

Decision Outcome

Only one option was considered.
@kanigsson kanigsson self-assigned this Sep 30, 2021
@kanigsson kanigsson added the generator Related to generator package (SPARK code generation) label Sep 30, 2021
@treiher treiher added this to To do in RecordFlux 0.6 via automation Sep 30, 2021
@treiher treiher moved this from To do to In progress in RecordFlux 0.6 Sep 30, 2021
kanigsson added a commit that referenced this issue Oct 1, 2021
@kanigsson
Remove cleanup code from Session.Initialize, add precondition
31e57fd 
We remove the defensive code from Session.Initialize, which
deallocates buffers for global session variables if already
allocated. We add a precondition "Session.Unitialized" to that
procedure to avoid calling it in such situations.

Fixes #788
@kanigsson kanigsson mentioned this issue Oct 1, 2021
Merged
kanigsson added a commit that referenced this issue Oct 1, 2021
@kanigsson
Remove cleanup code from Session.Initialize, add precondition
2bc63a6 
We remove the defensive code from Session.Initialize, which
deallocates buffers for global session variables if already
allocated. We add a precondition "Session.Unitialized" to that
procedure to avoid calling it in such situations.

Fixes #788
@senier senier moved this from In progress to Under review in RecordFlux 0.6 Oct 1, 2021
RecordFlux 0.6 automation moved this from Under review to Merged Oct 1, 2021
kanigsson added a commit that referenced this issue Oct 1, 2021
@kanigsson
Remove cleanup code from Session.Initialize, add precondition
9715402 
We remove the defensive code from Session.Initialize, which
deallocates buffers for global session variables if already
allocated. We add a precondition "Session.Unitialized" to that
procedure to avoid calling it in such situations.

Fixes #788
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@kanigsson kanigsson

Labels
generator Related to generator package (SPARK code generation)
Projects
No open projects
RecordFlux 0.6
  
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Remove cleanup code from Session.Initialize, add precondition AdaCore/RecordFlux
1 participant
@kanigsson