Rodin Index Design - Revision history

imported>Nicolas: /* Project save */ changed category "work in progress" to "work done"

2009-10-12T12:58:17Z

Project save: changed category "work in progress" to "work done"

← Older revision		Revision as of 12:58, 12 October 2009
Line 193:		Line 193:

	[[Category:Design]]		[[Category:Design]]
	[[Category:Work ~~in progress~~]]		[[Category:Work done]]

imported>Nicolas: /* Dependencies */ remove theorem terminology

2009-05-07T16:17:46Z

Dependencies: remove theorem terminology

← Older revision		Revision as of 16:17, 7 May 2009
Line 72:		Line 72:
	But having these dependencies is not precise enough, and can still lead to a lot of unnecessary indexing.		But having these dependencies is not precise enough, and can still lead to a lot of unnecessary indexing.

	<blockquote>For instance, in event-B, if the user adds ~~a theorem~~ to a context on which all files of a project depend (e.g., the context seen by the top-level machine of this project), then we would have to re-index all the files of the project, although it will be useless, as the ~~theorem~~ is not visible to the other files.</blockquote>		<blockquote>For instance, in event-B, if the user adds an axiom to a context on which all files of a project depend (e.g., the context seen by the top-level machine of this project), then we would have to re-index all the files of the project, although it will be useless, as the axiom is not visible to the other files.</blockquote>

	Therefore, we also ask that the indexer reports the declarations that are exported (i.e., made visible) by a file to the files that depend on it. This information is stored in the table specified as		Therefore, we also ask that the indexer reports the declarations that are exported (i.e., made visible) by a file to the files that depend on it. This information is stored in the table specified as

imported>Laurent at 09:08, 10 March 2009

2009-03-10T09:08:39Z

← Older revision		Revision as of 09:08, 10 March 2009
Line 132:		Line 132:
	* indexers have to read files from the database while they are potentially being modified concurrently (editing)		* indexers have to read files from the database while they are potentially being modified concurrently (editing)
	* the index can be queried while it is concurrently updated following to a database change		* the index can be queried while it is concurrently updated following to a database change


	===Queuing deltas===		===Queuing deltas===
Line 149:		Line 148:

	Cancellation can be requested through a popup that appears when the Job is taking too much time to complete, or from the progress view. Received at Job level, cancellation is propagated towards indexers, which are required to check it regularly and stop as soon as possible.		Cancellation can be requested through a popup that appears when the Job is taking too much time to complete, or from the progress view. Received at Job level, cancellation is propagated towards indexers, which are required to check it regularly and stop as soon as possible.


	===Exclusive database access===		===Exclusive database access===
Line 193:		Line 191:

	Stored contents are the same as for a workspace save, restricted to the project in question.		Stored contents are the same as for a workspace save, restricted to the project in question.



	[[Category:Design]]		[[Category:Design]]
	[[Category:Work in progress]]		[[Category:Work in progress]]

imported>Laurent at 09:07, 10 March 2009

2009-03-10T09:07:15Z

← Older revision		Revision as of 09:07, 10 March 2009
Line 138:		Line 138:
	The database delta mechanism requires that clients process change events quickly. Therefore, we cannot process database changes directly, but we rather queue them for later processing by the indexing thread. This is done through a blocking queue.		The database delta mechanism requires that clients process change events quickly. Therefore, we cannot process database changes directly, but we rather queue them for later processing by the indexing thread. This is done through a blocking queue.

	~~Also, another source of index updating needs is project~~ state changes (create/delete, open/close, clean)~~. Such changes~~ are also enqueued for later processing.		Project state changes (create/delete, open/close, clean) are also retrieved from the database delta mechanism and enqueued for later processing.

	Furthermore, blocking queues provide a thread-safe way to wait for deltas to arrive to the indexing thread, avoiding needless resource consumption with busy waiting.		Furthermore, blocking queues provide a thread-safe way to wait for deltas to arrive to the indexing thread, avoiding needless resource consumption with busy waiting.

imported>Nicolas: /* Workspace save */

2009-03-03T15:37:49Z

Workspace save

← Older revision		Revision as of 15:37, 3 March 2009
Line 178:		Line 178:
	* dependencies between files		* dependencies between files

	Moreover,the index manager must also persist its state, that is the list of deltas not yet fully processed when the platform shuts down. Upon startup, ~~this state~~ will be recovered and indexing resumed where it stopped.		Moreover,the index manager must also persist its state, that is
			* the list of deltas not yet fully processed when the platform shuts down
			* the indexer registry
			Upon startup, the delta list will be recovered and indexing resumed where it stopped.

			If the indexer registry changes (e.g. indexers added), a full indexing will be scheduled to update the index with the new indexer configuration.

	===Project save===		===Project save===

imported>Nicolas: /* Exclusive database access */

2009-03-03T15:28:02Z

Exclusive database access

← Older revision		Revision as of 15:28, 3 March 2009
Line 154:		Line 154:

	When indexers are given a file to index, we must be sure that it is not being modified concurrently. The database provides a way to manage exclusive access to its data, through Job scheduling rules. The interactive indexing job has to first acquire this exclusive lock, potentially waiting for others to finish (the builder for instance), before calling indexers.		When indexers are given a file to index, we must be sure that it is not being modified concurrently. The database provides a way to manage exclusive access to its data, through Job scheduling rules. The interactive indexing job has to first acquire this exclusive lock, potentially waiting for others to finish (the builder for instance), before calling indexers.

	Following the principle of separation between Index Manager and indexers, we considered the case where an indexer would keep running endlessly. So a timeout (30s) is put on the indexing of a single file by a single indexer, to prevent from irreparably freezing the whole platform.


	===Handling queries===		===Handling queries===

imported>Nicolas: /* Queuing deltas */

2009-03-03T15:20:06Z

Queuing deltas

← Older revision		Revision as of 15:20, 3 March 2009
Line 138:		Line 138:
	The database delta mechanism requires that clients process change events quickly. Therefore, we cannot process database changes directly, but we rather queue them for later processing by the indexing thread. This is done through a blocking queue.		The database delta mechanism requires that clients process change events quickly. Therefore, we cannot process database changes directly, but we rather queue them for later processing by the indexing thread. This is done through a blocking queue.

	Also, another source of index updating needs is project state changes (create/delete, open/close, clean). ~~These events are not sent by the Rodin database, but rather by the Resource plug-in (workspace listener).~~ Such changes are also enqueued for later processing.		Also, another source of index updating needs is project state changes (create/delete, open/close, clean). Such changes are also enqueued for later processing.

	Furthermore, blocking queues provide a thread-safe way to wait for deltas to arrive to the indexing thread, avoiding needless resource consumption with busy waiting.		Furthermore, blocking queues provide a thread-safe way to wait for deltas to arrive to the indexing thread, avoiding needless resource consumption with busy waiting.


	===Interactive indexing job===		===Interactive indexing job===

imported>Laurent: /* Concurrency */

2009-01-29T12:40:13Z

Concurrency

← Older revision		Revision as of 12:40, 29 January 2009
Line 127:		Line 127:
	Indexing should disturb the user experience as little as possible. Therefore, indexing must take place in a separate thread. This is achieved by using the Job API of Eclipse. All indexing takes place in a low-priority job.		Indexing should disturb the user experience as little as possible. Therefore, indexing must take place in a separate thread. This is achieved by using the Job API of Eclipse. All indexing takes place in a low-priority job.

	~~However, concurrency~~ problems might arise from several interactions:		Concurrency problems might arise from several interactions:
	* deltas are received asynchronously from the database		* deltas are received asynchronously from the database
	* the user should be able to cancel indexing if anything goes wrong		* the user should be able to cancel indexing if anything goes wrong

imported>Laurent: /* Concurrency */

2009-01-29T12:39:36Z

Concurrency

← Older revision		Revision as of 12:39, 29 January 2009
Line 125:		Line 125:
	==Concurrency==		==Concurrency==

	~~We need that indexing disturbs~~ as ~~less~~ as possible ~~the user experience~~. Therefore, indexing must take place in a separate thread. This is achieved by using the Job API of Eclipse. All indexing takes place in a low-priority job.		Indexing should disturb the user experience as little as possible. Therefore, indexing must take place in a separate thread. This is achieved by using the Job API of Eclipse. All indexing takes place in a low-priority job.

	However, several interactions ~~might cause concurrency issues~~:		However, concurrency problems might arise from several interactions:
	* deltas are received asynchronously from the database		* deltas are received asynchronously from the database
	* the user should be able to cancel indexing if anything goes wrong		* the user should be able to cancel indexing if anything goes wrong

imported>Laurent: /* Restrictions */

2009-01-29T12:36:14Z

Restrictions

← Older revision		Revision as of 12:36, 29 January 2009
Line 87:		Line 87:
	<blockquote><math>\mathit{file}\in\mathit{ELEMENT}\rel\mathit{FILE}</math> .</blockquote>		<blockquote><math>\mathit{file}\in\mathit{ELEMENT}\rel\mathit{FILE}</math> .</blockquote>

	This relation is a constant and is inherent to the database structure, it is not maintained by the index manager, only used by it.		This relation is a constant and is inherent to the database structure; it is not maintained by the index manager, only used by it.

	Firstly, we ask that an indexer running on file <math>f</math> contributes names only for elements belonging to this file, i.e., these elements must belong to set		Firstly, we ask that an indexer running on file <math>f</math> contributes names only for elements belonging to this file, i.e., these elements must belong to set
Line 109:		Line 109:

	Finally, an indexer can only export elements for which it can contribute occurrences, as detailed in the previous point.		Finally, an indexer can only export elements for which it can contribute occurrences, as detailed in the previous point.


	===Updating algorithm===		===Updating algorithm===