D23 Code Generation - Revision history

imported>Pascal: /* Timescales */

2009-12-07T18:07:35Z

Timescales

← Older revision		Revision as of 18:07, 7 December 2009
Line 135:		Line 135:
	*June 2011: prototype tool for V2.		*June 2011: prototype tool for V2.
	*From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots.		*From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots.

			[[Category:D23 Deliverable]]

imported>Pascal: /* Tasking Language */

2009-12-04T11:09:06Z

Tasking Language

← Older revision		Revision as of 11:09, 4 December 2009
Line 96:		Line 96:
	\|}		\|}

	A tasktype is used to indicate the scheduling requirements for the required activity. It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is ~~parametrised~~ by a time value. Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.		A tasktype is used to indicate the scheduling requirements for the required activity. It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parameterised by a time value. Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.
	It may be decided that, during a program’s execution, some of the activities should take precedence over some others. We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.		It may be decided that, during a program’s execution, some of the activities should take precedence over some others. We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.

imported>Pascal: /* Timescales */

2009-12-04T10:59:37Z

Timescales

← Older revision		Revision as of 10:59, 4 December 2009
Line 129:		Line 129:
	=Timescales=		=Timescales=
	We refer to the tasking language outlined above as Version V1. Our planned timescales for further work on code generation are as follows:		We refer to the tasking language outlined above as Version V1. Our planned timescales for further work on code generation are as follows:
	*June 2010: demonstrator tool for language V1		*June 2010: demonstrator tool for language V1.
	*June 2010: initial support for user defined datatypes (~~math extn~~)		*June 2010: initial support for user defined datatypes (mathematical extensions).
	*From June to October 2010: experimentation with and assessment of the demonstrator tool on the WP1 and WP3 pilots leading to feedback on V1 and the tool		*From June to October 2010: experimentation with and assessment of the demonstrator tool on the WP1 and WP3 pilots leading to feedback on V1 and the tool.
	*Jan 2011: algorithmic language definition V2		*Jan 2011: algorithmic language definition V2.
	*June 2011: prototype tool for V2		*June 2011: prototype tool for V2.
	*From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots		*From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots.

imported>Pascal: /* Tasking Language */

2009-12-04T10:57:46Z

Tasking Language

← Older revision		Revision as of 10:57, 4 December 2009
Line 77:		Line 77:
	The sequence, branching and iteration constructs correspond to their imperative counterparts. The task construct provides a means to specify the actions of interleaving, concurrent executions. A task may be implemented by an Ada task, or a thread in C. A task, in isolation, is a sequential program with clearly identified atomic steps, and each step corresponding to an atomic event.		The sequence, branching and iteration constructs correspond to their imperative counterparts. The task construct provides a means to specify the actions of interleaving, concurrent executions. A task may be implemented by an Ada task, or a thread in C. A task, in isolation, is a sequential program with clearly identified atomic steps, and each step corresponding to an atomic event.

	The standard machine construct provides the mechanism for sharing data between the executing tasks. The interaction between a task and a machine can be represented synchronized event composition as currently supported by the synchronised-event ~~plugin~~. The generated implementation will need to ensure that a task has mutually exclusive access to the variables represented in the machine. This is provided by a machine’s atomic events. A machine representing shared variables may be implemented by an Ada protected object, or in C by an explicit Mutex variable and appropriate lock acquisition.		The standard machine construct provides the mechanism for sharing data between the executing tasks. The interaction between a task and a machine can be represented synchronized event composition as currently supported by the synchronised-event plug-in. The generated implementation will need to ensure that a task has mutually exclusive access to the variables represented in the machine. This is provided by a machine’s atomic events. A machine representing shared variables may be implemented by an Ada protected object, or in C by an explicit Mutex variable and appropriate lock acquisition.

	To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority		To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority.
	{\| border="0"		{\| border="0"
	\|Task :=		\|Task :=
Line 96:		Line 96:
	\|}		\|}

	A tasktype is used to indicate the scheduling requirements for the required activity. It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is ~~parameterised~~ by a time value. Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.		A tasktype is used to indicate the scheduling requirements for the required activity. It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parametrised by a time value. Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.
	It may be decided that, during a program’s execution, some of the activities should take precedence over some others. We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.		It may be decided that, during a program’s execution, some of the activities should take precedence over some others. We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.

imported>Pascal: /* Choices/Decisions */

2009-12-04T10:54:30Z

Choices/Decisions

← Older revision		Revision as of 10:54, 4 December 2009
Line 8:		Line 8:
	The code generation work is being lead by Southampton with initial input from Newcastle.		The code generation work is being lead by Southampton with initial input from Newcastle.

	=Choices/Decisions=		=Choices / Decisions=
	Three candidate approaches have been posited as follows:		Three candidate approaches have been posited as follows:
	* Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation.		* Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation.

imported>Pascal: /* Choices/Decisions */

2009-12-04T10:53:38Z

Choices/Decisions

← Older revision		Revision as of 10:53, 4 December 2009
Line 9:		Line 9:

	=Choices/Decisions=		=Choices/Decisions=
	Three candidate approaches have been posited as follows;		Three candidate approaches have been posited as follows:
	• Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation		* Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation.
	• Synthesise sequential and concurrent code from existing low-level Event-B models		* Synthesise sequential and concurrent code from existing low-level Event-B models.
	• Exploit the code generation facilities of Atelier-B for “classical” B		* Exploit the code generation facilities of Atelier-B for “classical” B.

	Approach 3 will be important for STS in WP2 as it will enable integration of Rodin with the existing development process in STS with AtelierB and some effort will be devoted to this. However, this approach will not address the needs of all the deployments because of the overhead involved in having to use AtelierB alongside Rodin as well as the lack of support for concurrent code generation in AtelierB. Supporting Approach 2 has the attraction that developers can remain within the uniform language framework of Event-B. However, it is not clear that we can meet the real-time performance guarantees required for embedded systems with this approach within the lifetime of the DEPLOY project.		Approach 3 will be important for STS in WP2 as it will enable integration of Rodin with the existing development process in STS with AtelierB and some effort will be devoted to this. However, this approach will not address the needs of all the deployments because of the overhead involved in having to use AtelierB alongside Rodin as well as the lack of support for concurrent code generation in AtelierB. Supporting Approach 2 has the attraction that developers can remain within the uniform language framework of Event-B. However, it is not clear that we can meet the real-time performance guarantees required for embedded systems with this approach within the lifetime of the DEPLOY project.

imported>WikiSysop: /* Tasking Language */

2009-11-30T23:26:07Z

Tasking Language

← Older revision		Revision as of 23:26, 30 November 2009
Line 47:		Line 47:
	\|-		\|-
	\|		\|
	\| task Name		\| '''task''' Name
	\|-		\|-
	\|		\|
	\| variables Variables		\| '''variables''' Variables
	\|-		\|-
	\|		\|
	\| invariants Invariants		\| '''invariants''' Invariants
	\|-		\|-
	\|		\|
	\| begin TaskBody end		\| '''begin''' TaskBody '''end'''
	\|}		\|}

Line 84:		Line 84:
	\|-		\|-
	\|		\|
	\| task Name		\| '''task''' Name
	\|-		\|-
	\|		\|
	\| tasktype periodic(p) <math>\|</math> triggered <math>\|</math> repeating <math>\|</math> oneshot		\| '''tasktype''' '''periodic'''(p) <math>\|</math> '''triggered''' <math>\|</math> '''repeating''' <math>\|</math> '''oneshot'''
	\|-		\|-
	\|		\|
	\| priority n		\| '''priority''' n
	\|-		\|-
	\|		\|

imported>WikiSysop: /* Methodological Support */

2009-11-30T23:24:44Z

Methodological Support

← Older revision		Revision as of 23:24, 30 November 2009
Line 102:		Line 102:
	As previously outlined, the atomic steps of a sequential task will be syntactically explicit. This is in order to facilitate a direct mapping of task steps with events of an abstract machine. The development approach that we plan to support fits with the general refinement approach of Event-B in that explicit tasking will be introduced as part of a refinement step. A common approach to specifying a problem is to represent some desired outcome as a single abstract atomic event. Common patterns of refinement of such abstract events found in existing Event-B developments are as follows:		As previously outlined, the atomic steps of a sequential task will be syntactically explicit. This is in order to facilitate a direct mapping of task steps with events of an abstract machine. The development approach that we plan to support fits with the general refinement approach of Event-B in that explicit tasking will be introduced as part of a refinement step. A common approach to specifying a problem is to represent some desired outcome as a single abstract atomic event. Common patterns of refinement of such abstract events found in existing Event-B developments are as follows:

	*Choice refinement: Event E is refined to E1 [] E2 []…[] En, where each Ei refines E		#Choice refinement: Event E is refined to E1 [] E2 []…[] En, where each Ei refines E
	*Sequential refinement: Event E is refined to E1 ; E2 ; … En, where some Ei refines E and the other Ej refine skip.		#Sequential refinement: Event E is refined to E1 ; E2 ; … En, where some Ei refines E and the other Ej refine skip.
	*Loop refinement: Event E is refined to E1 ; do E2 od ; E3, where E3 refines E and E1 and E2 refine skip.		#Loop refinement: Event E is refined to E1 ; do E2 od ; E3, where E3 refines E and E1 and E2 refine skip.

	These patterns motivate a simpler subset of the tasking language as follows		These patterns motivate a simpler subset of the tasking language as follows

imported>WikiSysop at 23:23, 30 November 2009

2009-11-30T23:23:32Z

@@ Line 80: / Line 80: @@
 To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority
 A tasktype is used to indicate the scheduling requirements for the required activity.  It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parameterised by a time value.  Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype.  In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this.
 It may be decided that, during a program’s execution, some of the activities should take precedence over some others.  We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.
@@ Line 97: / Line 107: @@
 These patterns motivate a simpler subset of the tasking language as follows
-TaskBody ::=
+{| border="0"
-		Event
+| TaskBody :=
-		|  TaskBody  ;  TaskBody
+|-
-		|  if  ::=  Event  [] … []  Event  fi
-		|  do	Event  endwith  Event  od
+| Event
 Initially we will support refinement to this subset by providing special structure-introduction refinement rules in the manner of the refinement calculus.  We will also develop support for a generalisation of this set of rules in which the abstract model consists of a group of atomic events, with each event representing a different possible outcome.  An example use of such a group would be to have an event to represent the normal behaviour of some system feature and a separate event to represent the error behaviour of the feature.

imported>WikiSysop: /* Tasking Language */

2009-11-30T23:20:04Z

Tasking Language

← Older revision		Revision as of 23:20, 30 November 2009
Line 69:		Line 69:
	\|-		\|-
	\|		\|
	\| <math>\|</math>'''if''' Guard→ TaskBody [] … [] Guard→ TaskBody '''fi'''		\| <math>\|</math> '''if''' Guard→ TaskBody [] … [] Guard→ TaskBody '''fi'''
	\|-		\|-
	\|		\|
	\| <math>\|</math>'''do''' Guard→ TaskBody [] … [] Guard→ TaskBody '''od'''		\| <math>\|</math> '''do''' Guard→ TaskBody [] … [] Guard→ TaskBody '''od'''
	\|}		\|}