Implements a generic global sharing strategy for clause exchange. More...

#include <GenericGlobalSharing.hpp>

Inheritance diagram for GenericGlobalSharing:

Collaboration diagram for GenericGlobalSharing:

Public Member Functions
	GenericGlobalSharing (const std::shared_ptr< ClauseDatabase > &clauseDB, const std::vector< int > &subscriptions, const std::vector< int > &subscribers, unsigned long bufferSize)
	Constructor for GenericGlobalSharing with copy semantics.

	~GenericGlobalSharing ()
	Destructor for GenericGlobalSharing.

bool	initMpiVariables () override
	Initializes MPI-related variables.

bool	doSharing () override
	Performs the clause sharing operation. An MPI process starts by serializing its clauses then sends them via asynchronous sends to all its subscribers, then waits on the reception of its different subscriptions.

void	joinProcess (int winnerRank, SatResult res, const std::vector< int > &model) override
	Handles the process of joining when a solution is found.

Public Member Functions inherited from GlobalSharingStrategy
	GlobalSharingStrategy (const std::shared_ptr< ClauseDatabase > &clauseDB, const std::vector< std::shared_ptr< SharingEntity > > &producers={}, const std::vector< std::shared_ptr< SharingEntity > > &consumers={})
	Constructor for GlobalSharingStrategy.

virtual	~GlobalSharingStrategy ()
	Destructor.

bool	importClause (const ClauseExchangePtr &cls) override
	Imports a clause into the clause database.

void	importClauses (const std::vector< ClauseExchangePtr > &v_cls) override
	Imports multiple clauses into the clause database.

bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client)
	Exports a clause to a specific client.

std::chrono::microseconds	getSleepingTime () override
	Gets the sleeping time for the sharing strategy.

void	printStats () override
	Prints the statistics of the sharing strategy.

Public Member Functions inherited from SharingStrategy
	SharingStrategy (const std::vector< std::shared_ptr< SharingEntity > > &producers, const std::vector< std::shared_ptr< SharingEntity > > &consumers, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Constructor for SharingStrategy. Be sure to call connectConstructorProducers after construction, this is due to the base class shared_from_this.

virtual	~SharingStrategy ()
	Virtual destructor.

void	connectConstructorProducers ()
	Add this to the producers' clients list.

virtual void	addProducer (std::shared_ptr< SharingEntity > producer)
	Adds a producer to this strategy.

virtual void	connectProducer (std::shared_ptr< SharingEntity > producer)
	Connect a producer to this strategy. Add (this) to clients of (producer)

virtual void	removeProducer (std::shared_ptr< SharingEntity > producer)
	Removes a producer from this strategy.

Public Member Functions inherited from SharingEntity
	SharingEntity ()
	Construct a new SharingEntity object.

	SharingEntity (const std::vector< std::shared_ptr< SharingEntity > > &clients)
	Construct a new SharingEntity object.

virtual	~SharingEntity ()
	Destroy the SharingEntity object.

int	getSharingId () const
	Get the sharing ID of this entity.

void	setSharingId (int _id)
	Set the sharing ID of this entity.

virtual void	addClient (std::shared_ptr< SharingEntity > client)
	Add a client to this entity.

virtual void	removeClient (std::shared_ptr< SharingEntity > client)
	Remove a specific client from this entity.

size_t	getClientCount () const
	Get the current number of clients.

void	clearClients ()
	Remove all clients.

Protected Member Functions
int	serializeClauses (std::vector< int > &serialized_v_cls)
	Serializes clauses for sharing.

void	deserializeClauses (std::vector< int > &serialized_v_cls)
	Deserializes received clauses.

Protected Member Functions inherited from SharingStrategy
bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client) override
	A SharingStrategy doesn't send a clause to the source client (->from must store the sharingId of its producer)

Protected Member Functions inherited from SharingEntity
bool	exportClause (const ClauseExchangePtr &clause)
	Export a clause to all registered clients.

void	exportClauses (const std::vector< ClauseExchangePtr > &clauses)
	Export multiple clauses to all registered clients.

Protected Attributes
unsigned int	totalSize
	Total size of the buffer for clause sharing.

std::vector< MPI_Request >	sendRequests
	MPI requests for non-blocking sends.

BloomFilter	b_filter_send
	Bloom filter for avoiding duplicate clause sends.

BloomFilter	b_filter_recv
	Bloom filter for avoiding duplicate clause receives.

std::vector< int >	clausesToSendSerialized
	Buffer for serialized clauses to send.

std::vector< int >	receivedClauses
	Buffer for received serialized clauses.

std::vector< int >	subscriptions
	List of MPI ranks to receive clauses from.

std::vector< int >	subscribers
	List of MPI ranks to send clauses to.

Protected Attributes inherited from GlobalSharingStrategy
GlobalSharingStatistics	gstats
	Statistics for global sharing.

bool	requests_sent
	Flag indicating if requests to end were sent to the root.

std::vector< MPI_Request >	recv_end_requests
	MPI requests for non-blocking receive of end signals.

MPI_Request	send_end_request
	MPI request for non-root Isend for final synchronization with root.

std::vector< int >	receivedFinalResultRoot
	Buffer for storing results received from other mpi processes.

Protected Attributes inherited from SharingStrategy
std::shared_ptr< ClauseDatabase >	m_clauseDB
	Clause database where exported clauses are stored.

SharingStatistics	stats
	Sharing statistics.

std::vector< std::weak_ptr< SharingEntity > >	m_producers
	The set holding the references to the producers.

std::shared_mutex	m_producersMutex
	Shared mutex for producers list (to become RCU ?)

Protected Attributes inherited from SharingEntity
std::vector< std::weak_ptr< SharingEntity > >	m_clients
	List of weak pointers to client SharingEntities.

std::shared_mutex	m_clientsMutex
	Mutex to protect access to m_clients.

Detailed Description

Implements a generic global sharing strategy for clause exchange.

This class extends GlobalSharingStrategy to provide a generic implementation for clause sharing among MPI processes.

Constructor & Destructor Documentation

◆ GenericGlobalSharing()

GenericGlobalSharing::GenericGlobalSharing	(	const std::shared_ptr< ClauseDatabase > &	clauseDB,
		const std::vector< int > &	subscriptions,
		const std::vector< int > &	subscribers,
		unsigned long	bufferSize )

Constructor for GenericGlobalSharing with copy semantics.

Parameters

clauseDB	Shared pointer to the clause database.
subscriptions	Vector of MPI ranks to receive clauses from.
subscribers	Vector of MPI ranks to send clauses to.
bufferSize	Size of the buffer to send to subscribers

Member Function Documentation

◆ deserializeClauses()

void GenericGlobalSharing::deserializeClauses ( std::vector< int > & serialized_v_cls )

protected

Deserializes received clauses.

Parameters

serialized_v_cls Vector containing the serialized clauses.

◆ doSharing()

bool GenericGlobalSharing::doSharing ( )

overridevirtual

Performs the clause sharing operation. An MPI process starts by serializing its clauses then sends them via asynchronous sends to all its subscribers, then waits on the reception of its different subscriptions.

Returns: true if sharing is complete and the process can terminate, false otherwise.

Reimplemented from GlobalSharingStrategy.

◆ initMpiVariables()

bool GenericGlobalSharing::initMpiVariables ( )

overridevirtual

Initializes MPI-related variables.

Returns: true if initialization was successful, false otherwise.

Reimplemented from GlobalSharingStrategy.

◆ joinProcess()

void GenericGlobalSharing::joinProcess	(	int	winnerRank,
		SatResult	res,
		const std::vector< int > &	model )

overridevirtual

Handles the process of joining when a solution is found.

Parameters

winnerRank	The rank of the process that found the solution.
res	The result of the SAT solving process.
model	The satisfying assignment, if any.

Reimplemented from GlobalSharingStrategy.

◆ serializeClauses()

int GenericGlobalSharing::serializeClauses ( std::vector< int > & serialized_v_cls )

protected

Serializes clauses for sharing.

Parameters

serialized_v_cls Vector to store the serialized clauses.

Serialization Pattern ([size][lbd][literals])*

Returns: The number of clauses serialized.

The documentation for this class was generated from the following file:

/github/workspace/src/sharing/GlobalStrategies/GenericGlobalSharing.hpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ GenericGlobalSharing()

Member Function Documentation

◆ deserializeClauses()

◆ doSharing()

◆ initMpiVariables()

◆ joinProcess()

◆ serializeClauses()