---------- entry.cpp ----------

#include <divine.h>
#include <divine/problem.h>
#include <mpi.h>
#include <cstdlib>

int _mpi_num_processes = 0;
int _mpi_exit_barrier = 0;

extern "C" {
    int main(...);
    struct global_ctor { int prio; void (*fn)(); };

    int _divine_invoke_main( int mainproto )
    {
        switch ( mainproto ) {
            case 0: return main();
            case 1: return main( 0 );
            case 2: return main( 0, 0 );
            case 3: return main( 0, 0, 0 );
            default: __divine_problem( 1, "don't know how to run main()" );
        }
    }

    void _divine_invoke_main_mpi( void *mainproto )
    {
        // run main
        int r = _divine_invoke_main( *((int *) mainproto) );

        // check whether MPI_Finalize has been called
        int finalized; MPI_Finalized( &finalized );
        if ( !finalized ) {
            __divine_problem( Other,
                    "MPI_Finalize not called before program termination" );
        }

        // synchronize thread exits because it's needed apparently TODO desc
        __divine_interrupt_mask();
        ++_mpi_exit_barrier;

        while ( !(_mpi_exit_barrier == _mpi_num_processes &&
                __divine_get_tid() == 0) ) {
            __divine_interrupt_unmask();
            __divine_interrupt_mask();
        }

        exit( r ); // only thread 0 gets here
    }

    void _divine_start( int ctorcount, void *ctors, int mainproto )
    {
        global_ctor *c = reinterpret_cast< global_ctor * >( ctors );
        for ( int i = 0; i < ctorcount; ++i ) {
            c->fn();
            c ++;
        }

        if ( _mpi_num_processes == 0 ) {
            // normal startup (no MPI): run main in one thread
            int r = _divine_invoke_main( mainproto );
            exit( r );
        } else {
            // MPI startup: perform global MPI initialization...
            _divine_mpi_global_initialize();

            // ...and run main in the specified number of MPI processes (which
            // are implemented as threads currently)
            for ( int i = 0; i < _mpi_num_processes - 1; ++i ) {
                __divine_new_thread( _divine_invoke_main_mpi,
                        (void *) &mainproto );
            }
            _divine_invoke_main_mpi( (void *) &mainproto );
        }
    }
}

---------- mpi.cpp ----------

void _divine_mpi_global_initialize() {
    // initialize internal globals
    _initialized_ = new (nofail) bool[_mpi_num_processes] {};
    _finalized_ = new (nofail) bool[_mpi_num_processes] {};
    _buffer_attached_ = new (nofail) bool[_mpi_num_processes] {};

    assert(_mpi_num_processes == 2); //DEBUG

    _attached_buffer_ = new (nofail) char*[2/*_mpi_num_processes*/]; // {}; //XXX
    _attached_buffer_size_ = new (nofail) int[2/*_mpi_num_processes*/]; // {}; //XXX
    _queue_head_ = new (nofail) PMEHeader*[2/*_mpi_num_processes*/]; // {}; //XXX
    _queue_tail_ = new (nofail) char*[2/*_mpi_num_processes*/]; // {}; //XXX
    _num_entries_ = new (nofail) int[2/*_mpi_num_processes*/] {};

    // create predefined datatypes and reduction operations
    create_predefined_datatypes();
    create_predefined_reduction_operations();

    // create the empty group
    MPI_GROUP_EMPTY = new (nofail) _Group {};

    // prepare predefined communicators
    MPI_COMM_WORLD_ = new (nofail) MPI_Comm[2/*_mpi_num_processes*/] {}; //DEBUG
    MPI_COMM_SELF_ = new (nofail) MPI_Comm[2/*_mpi_num_processes*/] {}; //DEBUG
}