/**CFile**************************************************************** FileName [giaSat.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Scalable AIG package.] Synopsis [New constraint-propagation procedures.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: giaSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "gia.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define GIA_LIMIT 10 typedef struct Gia_ManSat_t_ Gia_ManSat_t; struct Gia_ManSat_t_ { Aig_MmFlex_t * pMem; }; typedef struct Gia_ObjSat1_t_ Gia_ObjSat1_t; struct Gia_ObjSat1_t_ { char nFans; char nOffset; char PathsH; char PathsV; }; typedef struct Gia_ObjSat2_t_ Gia_ObjSat2_t; struct Gia_ObjSat2_t_ { unsigned fTerm : 1; unsigned iLit : 31; }; typedef struct Gia_ObjSat_t_ Gia_ObjSat_t; struct Gia_ObjSat_t_ { union { Gia_ObjSat1_t Obj1; Gia_ObjSat2_t Obj2; }; }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_ManSat_t * Gia_ManSatStart() { Gia_ManSat_t * p; p = ABC_CALLOC( Gia_ManSat_t, 1 ); p->pMem = Aig_MmFlexStart(); return p; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSatStop( Gia_ManSat_t * p ) { Aig_MmFlexStop( p->pMem, 0 ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Collects the supergate rooted at this ] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSatPartCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLits, int * pnLits ) { Gia_Obj_t * pFanin; assert( Gia_ObjIsAnd(pObj) ); assert( pObj->fMark0 == 0 ); pFanin = Gia_ObjFanin0(pObj); if ( pFanin->fMark0 || Gia_ObjFaninC0(pObj) ) pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC0(pObj)); else Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits); pFanin = Gia_ObjFanin1(pObj); if ( pFanin->fMark0 || Gia_ObjFaninC1(pObj) ) pLits[(*pnLits)++] = Gia_Var2Lit(Gia_ObjId(p, pFanin), Gia_ObjFaninC1(pObj)); else Gia_ManSatPartCollectSuper(p, pFanin, pLits, pnLits); } /**Function************************************************************* Synopsis [Returns the number of words used.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManSatPartCreate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int * pObjPlace, int * pStore ) { Gia_Obj_t * pFanin; int i, nWordsUsed, nSuperSize = 0, Super[2*GIA_LIMIT]; // make sure this is a valid node assert( Gia_ObjIsAnd(pObj) ); assert( pObj->fMark0 == 0 ); // collect inputs to the supergate Gia_ManSatPartCollectSuper( p, pObj, Super, &nSuperSize ); assert( nSuperSize <= 2*GIA_LIMIT ); // create the root entry *pObjPlace = 0; ((Gia_ObjSat1_t *)pObjPlace)->nFans = Gia_Var2Lit( nSuperSize, 0 ); ((Gia_ObjSat1_t *)pObjPlace)->nOffset = pStore - pObjPlace; nWordsUsed = nSuperSize; for ( i = 0; i < nSuperSize; i++ ) { pFanin = Gia_ManObj( p, Gia_Lit2Var(Super[i]) ); if ( pFanin->fMark0 ) { ((Gia_ObjSat2_t *)(pStore + i))->fTerm = 1; ((Gia_ObjSat2_t *)(pStore + i))->iLit = Super[i]; } else { assert( Gia_LitIsCompl(Super[i]) ); nWordsUsed += Gia_ManSatPartCreate_rec( p, pFanin, pStore + i, pStore + nWordsUsed ); } } return nWordsUsed; } /**Function************************************************************* Synopsis [Creates part and returns the number of words used.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManSatPartCreate( Gia_Man_t * p, Gia_Obj_t * pObj, int * pStore ) { return 1 + Gia_ManSatPartCreate_rec( p, pObj, pStore, pStore + 1 ); } /**Function************************************************************* Synopsis [Count the number of internal nodes in the leaf-DAG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSatPartCountClauses( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnOnset, int * pnOffset ) { Gia_Obj_t * pFanin; int nOnset0, nOnset1, nOffset0, nOffset1; assert( Gia_ObjIsAnd(pObj) ); pFanin = Gia_ObjFanin0(pObj); if ( pFanin->fMark0 ) nOnset0 = 1, nOffset0 = 1; else { Gia_ManSatPartCountClauses(p, pFanin, &nOnset0, &nOffset0); if ( Gia_ObjFaninC0(pObj) ) { int Temp = nOnset0; nOnset0 = nOffset0; nOffset0 = Temp; } } pFanin = Gia_ObjFanin1(pObj); if ( pFanin->fMark0 ) nOnset1 = 1, nOffset1 = 1; else { Gia_ManSatPartCountClauses(p, pFanin, &nOnset1, &nOffset1); if ( Gia_ObjFaninC1(pObj) ) { int Temp = nOnset1; nOnset1 = nOffset1; nOffset1 = Temp; } } *pnOnset = nOnset0 * nOnset1; *pnOffset = nOffset0 + nOffset1; } /**Function************************************************************* Synopsis [Count the number of internal nodes in the leaf-DAG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int * pnNodes ) { Gia_Obj_t * pFanin; int Level0 = 0, Level1 = 0; assert( Gia_ObjIsAnd(pObj) ); assert( pObj->fMark0 == 0 ); (*pnNodes)++; pFanin = Gia_ObjFanin0(pObj); if ( pFanin->fMark0 ) (*pnLeaves)++; else Level0 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC0(pObj); pFanin = Gia_ObjFanin1(pObj); if ( pFanin->fMark0 ) (*pnLeaves)++; else Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj); return ABC_MAX( Level0, Level1 ); } /**Function************************************************************* Synopsis [Count the number of internal nodes in the leaf-DAG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManSatPartCountNodes( Gia_Man_t * p, Gia_Obj_t * pObj ) { Gia_Obj_t * pFanin; int nNodes0 = 0, nNodes1 = 0; assert( Gia_ObjIsAnd(pObj) ); assert( pObj->fMark0 == 0 ); pFanin = Gia_ObjFanin0(pObj); if ( !(pFanin->fMark0) ) nNodes0 = Gia_ManSatPartCountNodes(p, pFanin); pFanin = Gia_ObjFanin1(pObj); if ( !(pFanin->fMark0) ) nNodes1 = Gia_ManSatPartCountNodes(p, pFanin); return nNodes0 + nNodes1 + 1; } /**Function************************************************************* Synopsis [Count the number of internal nodes in the leaf-DAG.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSatPartPrint( Gia_Man_t * p, Gia_Obj_t * pObj, int Step ) { Gia_Obj_t * pFanin; assert( Gia_ObjIsAnd(pObj) ); assert( pObj->fMark0 == 0 ); pFanin = Gia_ObjFanin0(pObj); if ( pFanin->fMark0 ) printf( "%s%d", Gia_ObjFaninC0(pObj)?"!":"", Gia_ObjId(p,pFanin) ); else { if ( Gia_ObjFaninC0(pObj) ) printf( "(" ); Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC0(pObj)); if ( Gia_ObjFaninC0(pObj) ) printf( ")" ); } printf( "%s", (Step & 1)? " + " : "*" ); pFanin = Gia_ObjFanin1(pObj); if ( pFanin->fMark0 ) printf( "%s%d", Gia_ObjFaninC1(pObj)?"!":"", Gia_ObjId(p,pFanin) ); else { if ( Gia_ObjFaninC1(pObj) ) printf( "(" ); Gia_ManSatPartPrint(p, pFanin, Step + Gia_ObjFaninC1(pObj)); if ( Gia_ObjFaninC1(pObj) ) printf( ")" ); } } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManSatExperiment( Gia_Man_t * p ) { int nStored, Storage[1000], * pStart; Gia_ManSat_t * pMan; Gia_Obj_t * pObj; int i, nLevels, nLeaves, nNodes, nCount[2*GIA_LIMIT+2] = {0}, nCountAll = 0; int Num0 = 0, Num1 = 0; int clk = clock(), nWords = 0, nWords2 = 0; pMan = Gia_ManSatStart(); // mark the nodes to become roots of leaf-DAGs Gia_ManSetRefs( p ); Gia_ManForEachObj( p, pObj, i ) { pObj->fMark0 = 0; if ( Gia_ObjIsCo(pObj) ) Gia_ObjFanin0(pObj)->fMark0 = 1; else if ( Gia_ObjIsCi(pObj) ) pObj->fMark0 = 1; else if ( Gia_ObjIsAnd(pObj) ) { if ( pObj->Value > 1 || Gia_ManSatPartCountNodes(p,pObj) >= GIA_LIMIT ) pObj->fMark0 = 1; } pObj->Value = 0; } // compute the sizes of leaf-DAGs Gia_ManForEachAnd( p, pObj, i ) { if ( pObj->fMark0 == 0 ) continue; pObj->fMark0 = 0; nCountAll++; nStored = Gia_ManSatPartCreate( p, pObj, Storage ); nWords2 += nStored; assert( nStored < 500 ); pStart = (int *)Aig_MmFlexEntryFetch( pMan->pMem, sizeof(int) * nStored ); memcpy( pStart, Storage, sizeof(int) * nStored ); nLeaves = nNodes = 0; nLevels = 1+Gia_ManSatPartCount( p, pObj, &nLeaves, &nNodes ); nWords += nLeaves + nNodes; if ( nNodes <= 2*GIA_LIMIT ) nCount[nNodes]++; else nCount[2*GIA_LIMIT+1]++; // if ( nNodes > 10 && i % 100 == 0 ) // if ( nNodes > 5 ) if ( 0 ) { Gia_ManSatPartCountClauses( p, pObj, &Num0, &Num1 ); printf( "%8d : And = %3d. Lev = %2d. Clauses = %3d. (%3d + %3d).\n", i, nNodes, nLevels, Num0+Num1, Num0, Num1 ); Gia_ManSatPartPrint( p, pObj, 0 ); printf( "\n" ); } pObj->fMark0 = 1; } printf( "\n" ); Gia_ManForEachObj( p, pObj, i ) pObj->fMark0 = 0; Gia_ManSatStop( pMan ); for ( i = 0; i < 2*GIA_LIMIT+2; i++ ) printf( "%2d=%6d %7.2f %% %7.2f %%\n", i, nCount[i], 100.0*nCount[i]/nCountAll, 100.0*i*nCount[i]/Gia_ManAndNum(p) ); ABC_PRM( "MemoryEst", 4*nWords ); ABC_PRM( "MemoryReal", 4*nWords2 ); printf( "%5.2f bpn ", 4.0*nWords2/Gia_ManObjNum(p) ); ABC_PRT( "Time", clock() - clk ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END n218'>218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 
--- a/drivers/mtd/devices/block2mtd.c
+++ b/drivers/mtd/devices/block2mtd.c
@@ -29,6 +29,8 @@ struct block2mtd_dev {
 	struct block_device *blkdev;
 	struct mtd_info mtd;
 	struct mutex write_mutex;
+	rwlock_t bdev_mutex;
+	char devname[0];
 };
 
 
@@ -79,6 +81,12 @@ static int block2mtd_erase(struct mtd_in
 	size_t len = instr->len;
 	int err;
 
+	read_lock(&dev->bdev_mutex);
+	if (!dev->blkdev) {
+		err = -EINVAL;
+		goto done;
+	}
+
 	instr->state = MTD_ERASING;
 	mutex_lock(&dev->write_mutex);
 	err = _block2mtd_erase(dev, from, len);
@@ -90,6 +98,10 @@ static int block2mtd_erase(struct mtd_in
 		instr->state = MTD_ERASE_DONE;
 
 	mtd_erase_callback(instr);
+
+done:
+	read_unlock(&dev->bdev_mutex);
+
 	return err;
 }
 
@@ -101,7 +113,13 @@ static int block2mtd_read(struct mtd_inf
 	struct page *page;
 	int index = from >> PAGE_SHIFT;
 	int offset = from & (PAGE_SIZE-1);
-	int cpylen;
+	int cpylen, err = 0;
+
+	read_lock(&dev->bdev_mutex);
+	if (!dev->blkdev || (from > mtd->size)) {
+		err = -EINVAL;
+		goto done;
+	}
 
 	while (len) {
 		if ((offset + len) > PAGE_SIZE)
@@ -111,8 +129,10 @@ static int block2mtd_read(struct mtd_inf
 		len = len - cpylen;
 
 		page = page_read(dev->blkdev->bd_inode->i_mapping, index);
-		if (IS_ERR(page))
+		if (IS_ERR(page)) {
 			return PTR_ERR(page);
+			goto done;
+		}
 
 		memcpy(buf, page_address(page) + offset, cpylen);
 		page_cache_release(page);
@@ -123,7 +143,10 @@ static int block2mtd_read(struct mtd_inf
 		offset = 0;
 		index++;
 	}
-	return 0;
+
+done:
+	read_unlock(&dev->bdev_mutex);
+	return err;
 }
 
 
@@ -171,13 +194,22 @@ static int block2mtd_write(struct mtd_in
 		size_t *retlen, const u_char *buf)
 {
 	struct block2mtd_dev *dev = mtd->priv;
-	int err;
+	int err = 0;
+
+	read_lock(&dev->bdev_mutex);
+	if (!dev->blkdev) {
+		err = -EINVAL;
+		goto done;
+	}
 
 	mutex_lock(&dev->write_mutex);
 	err = _block2mtd_write(dev, buf, to, len, retlen);
 	mutex_unlock(&dev->write_mutex);
 	if (err > 0)
 		err = 0;
+
+done:
+	read_unlock(&dev->bdev_mutex);
 	return err;
 }
 
@@ -186,33 +218,110 @@ static int block2mtd_write(struct mtd_in
 static void block2mtd_sync(struct mtd_info *mtd)
 {
 	struct block2mtd_dev *dev = mtd->priv;
+	read_lock(&dev->bdev_mutex);
+	if (dev->blkdev)
 	sync_blockdev(dev->blkdev);
+	read_unlock(&dev->bdev_mutex);
+
 	return;
 }
 
 
+static int _open_bdev(struct block2mtd_dev *dev)
+{
+	const fmode_t mode = FMODE_READ | FMODE_WRITE | FMODE_EXCL;
+	struct block_device *bdev;
+
+	/* Get a handle on the device */
+	bdev = blkdev_get_by_path(dev->devname, mode, dev);
+#ifndef MODULE
+	if (IS_ERR(bdev)) {
+		dev_t devt;
+
+		/* We might not have rootfs mounted at this point. Try
+		   to resolve the device name by other means. */
+
+		devt = name_to_dev_t(dev->devname);
+		if (devt)
+			bdev = blkdev_get_by_dev(devt, mode, dev);
+	}
+#endif
+
+	if (IS_ERR(bdev)) {
+		ERROR("error: cannot open device %s", dev->devname);
+		return 1;
+	}
+	dev->blkdev = bdev;
+
+	if (MAJOR(bdev->bd_dev) == MTD_BLOCK_MAJOR) {
+		ERROR("attempting to use an MTD device as a block device");
+		return 1;
+	}
+
+	return 0;
+}
+
+static void _close_bdev(struct block2mtd_dev *dev)
+{
+	struct block_device *bdev;
+
+	if (!dev->blkdev)
+		return;
+
+	bdev = dev->blkdev;
+	invalidate_mapping_pages(dev->blkdev->bd_inode->i_mapping, 0, -1);
+	blkdev_put(dev->blkdev, FMODE_READ|FMODE_WRITE|FMODE_EXCL);
+	dev->blkdev = NULL;
+}
+
 static void block2mtd_free_device(struct block2mtd_dev *dev)
 {
 	if (!dev)
 		return;
 
 	kfree(dev->mtd.name);
-
-	if (dev->blkdev) {
-		invalidate_mapping_pages(dev->blkdev->bd_inode->i_mapping,
-					0, -1);
-		blkdev_put(dev->blkdev, FMODE_READ|FMODE_WRITE|FMODE_EXCL);
-	}
-
+	_close_bdev(dev);
 	kfree(dev);
 }
 
 
-/* FIXME: ensure that mtd->size % erase_size == 0 */
-static struct block2mtd_dev *add_device(char *devname, int erase_size, const char *mtdname)
+static int block2mtd_refresh(struct mtd_info *mtd)
 {
-	const fmode_t mode = FMODE_READ | FMODE_WRITE | FMODE_EXCL;
+	struct block2mtd_dev *dev = mtd->priv;
 	struct block_device *bdev;
+	dev_t devt;
+	int err = 0;
+
+	/* no other mtd function can run at this point */
+	write_lock(&dev->bdev_mutex);
+
+	/* get the device number for the whole disk */
+	devt = MKDEV(MAJOR(dev->blkdev->bd_dev), 0);
+
+	/* close the old block device */
+	_close_bdev(dev);
+
+	/* open the whole disk, issue a partition rescan, then */
+	bdev = blkdev_get_by_dev(devt, FMODE_WRITE | FMODE_READ, mtd);
+	if (!bdev || !bdev->bd_disk)
+		err = -EINVAL;
+#ifndef CONFIG_MTD_BLOCK2MTD_MODULE
+	else
+		err = rescan_partitions(bdev->bd_disk, bdev);
+#endif
+	if (bdev)
+		blkdev_put(bdev, FMODE_READ|FMODE_WRITE|FMODE_EXCL);
+
+	/* try to open the partition block device again */
+	_open_bdev(dev);
+	write_unlock(&dev->bdev_mutex);
+
+	return err;
+}
+
+/* FIXME: ensure that mtd->size % erase_size == 0 */
+static struct block2mtd_dev *add_device(char *devname, int erase_size, char *mtdname)
+{
 	struct block2mtd_dev *dev;
 	struct mtd_partition *part;
 	char *name;
@@ -220,36 +329,17 @@ static struct block2mtd_dev *add_device(
 	if (!devname)
 		return NULL;
 
-	dev = kzalloc(sizeof(struct block2mtd_dev), GFP_KERNEL);
+	dev = kzalloc(sizeof(struct block2mtd_dev) + strlen(devname) + 1, GFP_KERNEL);
 	if (!dev)
 		return NULL;
 
-	/* Get a handle on the device */
-	bdev = blkdev_get_by_path(devname, mode, dev);
-#ifndef MODULE
-	if (IS_ERR(bdev)) {
+	strcpy(dev->devname, devname);
 
-		/* We might not have rootfs mounted at this point. Try
-		   to resolve the device name by other means. */
-
-		dev_t devt = name_to_dev_t(devname);
-		if (devt)
-			bdev = blkdev_get_by_dev(devt, mode, dev);
-	}
-#endif
-
-	if (IS_ERR(bdev)) {
-		ERROR("error: cannot open device %s", devname);
-		goto devinit_err;
-	}
-	dev->blkdev = bdev;
-
-	if (MAJOR(bdev->bd_dev) == MTD_BLOCK_MAJOR) {
-		ERROR("attempting to use an MTD device as a block device");
+	if (_open_bdev(dev))
 		goto devinit_err;
-	}
 
 	mutex_init(&dev->write_mutex);
+	rwlock_init(&dev->bdev_mutex);
 
 	/* Setup the MTD structure */
 	/* make the name contain the block device in */
@@ -274,6 +364,7 @@ static struct block2mtd_dev *add_device(
 	dev->mtd._read = block2mtd_read;
 	dev->mtd.priv = dev;
 	dev->mtd.owner = THIS_MODULE;
+	dev->mtd.refresh_device = block2mtd_refresh;
 
 	part = kzalloc(sizeof(struct mtd_partition), GFP_KERNEL);
 	part->name = name;