Indexing System - Revision history

imported>Nicolas: /* The Index Manager */

2009-03-09T17:41:25Z

The Index Manager

← Older revision		Revision as of 17:41, 9 March 2009
Line 22:		Line 22:
	* indexing files in computed order to update [[#Index Tables\|index tables]]		* indexing files in computed order to update [[#Index Tables\|index tables]]

	Finally, when the session closes, index data is saved (see [[#Persistence\|Persistence]] ~~hereafer~~) and the background job is cancelled.		Finally, when the session closes, index data is saved (see [[#Persistence\|Persistence]] hereafter) and the background job is cancelled.

	The IndexManager is also the entry point for index ~~requesting~~.		The IndexManager is also the entry point for index querying.

imported>Mathieu: /* Jobs and Locks */

2009-03-03T22:11:49Z

Jobs and Locks

← Older revision		Revision as of 22:11, 3 March 2009
Line 151:		Line 151:
	During indexing, resources must be left unchanged. However, it would be too costly to lock the whole RodinDB. Therefore, we only use the scheduling rule of the file to index, forcing the indexing job to wait until it is released. If another file is changed meanwhile, a delta will be generated and the modification will eventually be taken into account by the index manager.		During indexing, resources must be left unchanged. However, it would be too costly to lock the whole RodinDB. Therefore, we only use the scheduling rule of the file to index, forcing the indexing job to wait until it is released. If another file is changed meanwhile, a delta will be generated and the modification will eventually be taken into account by the index manager.

	Restoring and saving index data (see [[#Persistence]]) may lead to concurrency issues if deltas or queries were to be processed at the same time. Protection is achieved by synchronized methods in IndexManager (persistence and queries) and in PIMs (read/write access to index tables).		Restoring and saving index data (see [[#Persistence\|Persistence]] here before) may lead to concurrency issues if deltas or queries were to be processed at the same time. Protection is achieved by synchronized methods in IndexManager (persistence and queries) and in PIMs (read/write access to index tables).


	[[Category:Design]]		[[Category:Design]]

imported>Mathieu: /* The Index Manager */ link alt text

2009-03-03T22:11:02Z

The Index Manager: link alt text

← Older revision		Revision as of 22:11, 3 March 2009
Line 16:		Line 16:
	==The Index Manager==		==The Index Manager==

	'''IndexManager''' is the master class of the plug-in. There resides the ''start()'' method called in a background job at plug-in startup. Firstly, it restores saved index data from previous session (see [[#Persistence]]). Then it loops, waiting for database deltas to be enqueued and launching the indexing of changed files via a user-cancellable job (see [[#Concurrency]]).		'''IndexManager''' is the master class of the plug-in. There resides the ''start()'' method called in a background job at plug-in startup. Firstly, it restores saved index data from previous session (see [[#Persistence\|Persistence]] hereafter). Then it loops, waiting for database deltas to be enqueued and launching the indexing of changed files via a user-cancellable job (see [[#Concurrency\|Concurrency]] hereafter).

	Indexing is done in two steps, project per project:		Indexing is done in two steps, project per project:
Line 22:		Line 22:
	* indexing files in computed order to update [[#Index Tables\|index tables]]		* indexing files in computed order to update [[#Index Tables\|index tables]]

	Finally, when the session closes, index data is saved (see [[#Persistence]]) and the background job is cancelled.		Finally, when the session closes, index data is saved (see [[#Persistence\|Persistence]] hereafer) and the background job is cancelled.

	The IndexManager is also the entry point for index requesting.		The IndexManager is also the entry point for index requesting.

imported>Nicolas: /* Jobs and Locks */

2009-03-03T16:34:11Z

Jobs and Locks

← Older revision		Revision as of 16:34, 3 March 2009
Line 149:		Line 149:
	The IndexManager starts as a background job with low priority, then launches a user-cancelable indexing job at each delta processing.		The IndexManager starts as a background job with low priority, then launches a user-cancelable indexing job at each delta processing.

	During indexing~~, which potentially involves several projects~~, resources must be left unchanged. Therefore, we use the ~~RodinDB~~ scheduling rule to ~~lock it entirely~~, forcing the indexing job to wait until it is released.		During indexing, resources must be left unchanged. However, it would be too costly to lock the whole RodinDB. Therefore, we only use the scheduling rule of the file to index, forcing the indexing job to wait until it is released. If another file is changed meanwhile, a delta will be generated and the modification will eventually be taken into account by the index manager.

			Restoring and saving index data (see [[#Persistence]]) may lead to concurrency issues if deltas or queries were to be processed at the same time. Protection is achieved by synchronized methods in IndexManager (persistence and queries) and in PIMs (read/write access to index tables).

	Restoring and saving index data (see [[#Persistence]]) may lead to concurrency issues if deltas or requests were to be processed at the same time. Protection is achieved by locks in IndexManager (restore and requests), in PIMs (read/write access to index tables) and in PersistenceManager (project save).
	~~Full save is left unlocked, as no deltas or requests can occur during session closure.~~

	[[Category:Design]]		[[Category:Design]]

imported>Nicolas: /* Delta Queue */

2009-03-03T16:19:19Z

Delta Queue

← Older revision		Revision as of 16:19, 3 March 2009
Line 142:		Line 142:
	The '''DeltaQueue''', used by the IndexManager, is the place where deltas sent by the database are temporarily stored, waiting to be processed. '''DeltaQueuer''' is the listener. Actually, deltas are not enqueued "as is", but as '''IndexDelta''', that is a IRodinElement (file or project) plus a '''Kind''' (file changed, project closed …).		The '''DeltaQueue''', used by the IndexManager, is the place where deltas sent by the database are temporarily stored, waiting to be processed. '''DeltaQueuer''' is the listener. Actually, deltas are not enqueued "as is", but as '''IndexDelta''', that is a IRodinElement (file or project) plus a '''Kind''' (file changed, project closed …).

	To properly handle index ~~requests~~, we have to be in a stable state, waiting until the queue is empty. This is achieved by a '''CountUpDownLatch''' that counts the number of elements in the queue. It is incremented when an element is added and decremented when an element has been removed '''and processed'''.		To properly handle index queries, we have to be in a stable state, waiting until the queue is empty. This is achieved by a '''CountUpDownLatch''' that counts the number of elements in the queue. It is incremented when an element is added and decremented when an element has been removed '''and processed'''.


	===Jobs and Locks===		===Jobs and Locks===

imported>Nicolas: /* Dependencies */

2009-03-03T16:14:35Z

Dependencies

← Older revision		Revision as of 16:14, 3 March 2009
Line 71:		Line 71:
	==Dependencies==		==Dependencies==

	File dependencies are treated generically in the '''org.rodinp.internal.core.~~index~~.sort''' package. The final goal is to maintain an iterable [[#Total Order\|total order]] on the files of each project. PIMs will then follow this order when indexing their project, using type ''IRodinFile'' for generic parameter T.		File dependencies are treated generically in the '''org.rodinp.internal.core.indexer.sort''' package. The final goal is to maintain an iterable [[#Total Order\|total order]] on the files of each project. PIMs will then follow this order when indexing their project, using type ''IRodinFile'' for generic parameter T.

	===Node===		===Node===
Line 103:		Line 103:
	'''SortedNodes''' maintains a list of iterable sorted nodes. It delegates sorting to a '''Sorter'''.		'''SortedNodes''' maintains a list of iterable sorted nodes. It delegates sorting to a '''Sorter'''.

	An important feature is that, if the graph is modified during iteration, it restarts from the first node that differs between previous order and new order. To that end, iterated nodes are recorded.		An important feature is that, if the graph is modified during iteration, it restarts from the first node that differs between previous order and new order. To that end, iterated nodes are recorded.

	==Indexing Bridge==		==Indexing Bridge==

imported>Nicolas: /* General structure of the package */

2009-03-03T16:10:07Z

General structure of the package

← Older revision		Revision as of 16:10, 3 March 2009
Line 7:		Line 7:
	The indexer plug-in is made of the following packages:		The indexer plug-in is made of the following packages:

	* '''org.rodinp.core.~~index~~''': public interfaces and Plugin class		* '''org.rodinp.core.indexer''': public interfaces and Plugin class
	* '''org.rodinp.internal.core.~~index~~''': implementation of public interfaces and main classes (including '''IndexManager''')		* '''org.rodinp.internal.core.indexer''': implementation of public interfaces and main classes (including '''IndexManager''')
	* '''org.rodinp.internal.core.~~index~~.tables''': index tables (memory storage)		* '''org.rodinp.internal.core.indexer.tables''': index tables (memory storage)
	* '''org.rodinp.internal.core.~~index~~.sort''': generical sorting support (used to manage file dependencies)		* '''org.rodinp.internal.core.indexer.sort''': generical sorting support (used to manage file dependencies)
	* '''org.rodinp.internal.core.~~index~~.persistence''': index saving main classes (disk storage)		* '''org.rodinp.internal.core.indexer.persistence''': index saving main classes (disk storage)
	* '''org.rodinp.internal.core.~~index~~.persistence.xml''': index saving in xml (Strategy pattern)		* '''org.rodinp.internal.core.indexer.persistence.xml''': index saving in xml (Strategy pattern)


	==The Index Manager==		==The Index Manager==

imported>Nicolas: /* Indexing Bridge */

2008-12-19T10:23:14Z

Indexing Bridge

← Older revision		Revision as of 10:23, 19 December 2008
Line 113:		Line 113:

	This role gives it the responsibility to enforce constraints like:		This role gives it the responsibility to enforce constraints like:
	* an element ~~occurrence~~ cannot have an occurrence if it has not been declared before		* an element cannot have an occurrence if it has not been declared before
	* an element cannot be declared more than once		* an element cannot be declared more than once
	* declared elements must be local to the file		* declared elements must be local to the file
	* occurring elements must be either local or imported		* occurring elements must be either local or imported
			* declared elements should have one or more occurrences when indexing completes

			This last constraint aims at avoiding to store declarations that are never referred to. An element with no occurrence will therefore be removed from the indexing result before returning it to the FIM.

	==Persistence==		==Persistence==

imported>Nicolas: /* Indexing Bridge */

2008-12-18T16:59:36Z

Indexing Bridge

← Older revision		Revision as of 16:59, 18 December 2008
Line 108:		Line 108:
	==Indexing Bridge==		==Indexing Bridge==

	The '''IndexingBridge''' acts as a kind of a go-between during the indexing of a single file. It is built by the ~~PIM~~, then sent to indexers ~~through the FIM~~. Indexers get the file to index from it, then they fill it with declarations and occurrences. From these, the IndexingBridge builds an '''IndexingResult''' that is sent back to the PIM ~~(through the FIM again)~~.		The '''IndexingBridge''' acts as a kind of a go-between during the indexing of a single file. It is built by the FIM, then sent to indexers. Indexers get the file to index from it, then they fill it with declarations and occurrences. From these, the IndexingBridge builds an '''IndexingResult''' that is sent back to the FIM, then processed by the PIM.

	Thus, IndexingBridge is a path from and to the indexing system, from indexers point of view.		Thus, IndexingBridge is a path from and to the indexing system, from indexers point of view.

imported>Mathieu: Category:Developer documentation is parent category of Design

2008-12-18T10:48:18Z

Category:Developer documentation is parent category of Design

← Older revision		Revision as of 10:48, 18 December 2008
Line 154:		Line 154:

	[[Category:Design]]		[[Category:Design]]
	~~[[Category:Developer documentation]]~~